Library hydras.Schutte.Ordering_Functions
Ordering functions (after Schutte)
Pierre Casteran, LaBRI, University of Bordeaux
Every subset A of Ord can be enumerated in an unique way
by a segment of Ord.
Thus it makes sense to consider the alpha-th element of A
This module shows the construction of the ordering function of A, following
Schutte's definitions.
From ZornsLemma Require Import CountableTypes.
From hydras Require Export Schutte_basics.
Import Ensembles Well_Orders Countable PartialFun.
Import Classical MoreEpsilonIota Epsilon.
Set Implicit Arguments.
Definition segment (A: Ensemble Ord) :=
∀ alpha beta, In A alpha → beta < alpha → In A beta.
Definition proper_segment (A: Ensemble Ord) :=
segment A ∧ ¬ Same_set A ordinal.
Class ordering_function (f : Ord → Ord)
(A B : Ensemble Ord) : Prop :=
Build_OF {
OF_segment : segment A;
OF_total : ∀ a, In A a → In B (f a);
OF_onto : ∀ b, In B b → ∃ a, In A a ∧ f a = b;
OF_mono : ∀ a b, In A a → In A b → a < b → f a < f b
}.
Definition ordering_segment (A B : Ensemble Ord) :=
∃ f : Ord → Ord, ordering_function f A B.
Definition the_ordering_segment (B : Ensemble Ord) :=
the (fun x ⇒ ordering_segment x B).
Definition ord (B : Ensemble Ord) :=
some (fun f ⇒ ordering_function f (the_ordering_segment B) B).
Definition proper_segment_of (B : Ensemble Ord)(beta : Ord): Ensemble Ord :=
fun alpha ⇒ In B alpha ∧ alpha < beta ∧ In B beta.
Definition normal (f : Ord → Ord)(B : Ensemble Ord): Prop :=
ordering_function f ordinal B ∧ continuous f ordinal B.
Definition fun_equiv (f g : Ord → Ord)(A B : Ensemble Ord) :=
Same_set A B ∧ ∀ a, In A a → f a = g a.
Lemma ordinal_segment : segment ordinal.
Lemma members_proper (alpha : Ord) :
proper_segment (members alpha).
Lemma proper_members (A: Ensemble Ord) (H : proper_segment A) :
∃ a: Ord, Same_set A (members a).
Lemma countable_segment_proper : ∀ A : Ensemble Ord,
segment A → Countable A → proper_segment A.
Lemma ordering_function_In f A B a :
ordering_function f A B → In A a → In B (f a).
Lemma ordering_function_mono (f : Ord → Ord) (A B: Ensemble Ord) :
ordering_function f A B →
∀ alpha beta,
In A alpha → In A beta → alpha < beta → f alpha < f beta.
#[global] Hint Resolve ordering_function_mono : schutte.
Lemma ordering_function_mono_weak (f : Ord → Ord) (A B: Ensemble Ord) :
ordering_function f A B →
∀ a b, In A a → In A b → a ≤ b → f a ≤ f b.
#[global] Hint Resolve ordering_function_mono_weak : schutte.
Lemma ordering_function_monoR : ∀ f A B, ordering_function f A B →
∀ a b, In A a → In A b → f a < f b → a < b.
#[global] Hint Resolve ordering_function_monoR : schutte.
Lemma Ordering_bijection : ∀ f A B, ordering_function f A B →
fun_bijection A B f.
Lemma ordering_function_mono_weakR :
∀ f A B, ordering_function f A B →
∀ a b, In A a → In A b → f a ≤ f b → a ≤ b.
#[global] Hint Resolve ordering_function_mono_weakR : schutte.
Lemma ordering_function_seg : ∀ A B, ordering_segment A B →
segment A.
Lemma empty_ordering : ∀ B, (∀ b, ¬ B b) →
ordering_function (fun o ⇒ o)
(members zero)
B.
Lemma segment_lt : ∀ A a b, segment A → A a → b < a → A b.
Theorem segment_unbounded : ∀ A:Ensemble Ord, segment A →
Unbounded A →
A = ordinal.
Theorem ordering_le : ∀ f A B,
ordering_function f A B →
∀ alpha, In A alpha → alpha ≤ f alpha.
Section ordering_function_unicity.
Variables B A1 A2 : Ensemble Ord.
Variables f1 f2 : Ord → Ord.
Hypothesis O1 : ordering_function f1 A1 B.
Hypothesis O2 : ordering_function f2 A2 B.
Theorem ordering_function_unicity : fun_equiv f1 f2 A1 A2.
End ordering_function_unicity.
Lemma ordering_function_seg_unicity : ∀ A1 A2 B,
ordering_segment A1 B →
ordering_segment A2 B → A1 = A2.
Let us build now an ordering function, and the associated ordering segment
of any subset B composed of ordinals
Lemma proper_of_proper : ∀ B beta beta',
ordinal beta → In B beta →
In (proper_segment_of B beta) beta' →
proper_segment_of B beta' =
proper_segment_of (proper_segment_of B beta) beta'.
Section building_ordering_function_1.
Variable B : Ensemble Ord.
Hypothesis H_B : ∀ beta, In B beta →
∃! A : Ensemble Ord,
ordering_segment A
(proper_segment_of B beta).
Section beta_fixed.
Variable beta : Ord.
Hypothesis beta_B : In B beta.
Let us build an ordering function for (proper_segment_of B beta)
Definition _A := the (fun E ⇒
ordering_segment E (proper_segment_of B beta)).
Definition _f := some (fun f ⇒
ordering_function f _A
(proper_segment_of B beta)).
Lemma of_beta' : ordering_function _f _A (proper_segment_of B beta).
Remark Bbeta_denum : Countable (proper_segment_of B beta).
#[local] Hint Resolve of_beta': schutte.
Remark A_denum : Countable _A.
Lemma Proper_A : proper_segment _A.
Lemma g_def1 : ∃ g_beta: Ord, ordinal g_beta ∧ _A = members g_beta.
Lemma g_unic : ∀ g_beta g_beta', ordinal g_beta →
ordinal g_beta' →
_A = members g_beta →
_A = members g_beta' →
g_beta = g_beta'.
Definition g := iota inh_Ord (fun o ⇒ ordinal o ∧ _A = members o).
End beta_fixed.
Lemma g_def : ∀ beta, In B beta → _A beta = members (g beta ).
Lemma g_lemma :
∀ beta, In B beta →
ordering_function (_f beta) (members (g beta))
(proper_segment_of B beta).
Lemma g_mono : ∀ beta1 beta2, In B beta1 → In B beta2 →
beta1 < beta2 →
g beta1 < g beta2.
Lemma L3a : segment (image B g).
Lemma g_bij : fun_bijection B (image B g) g.
#[local] Hint Resolve g_bij : schutte.
Let g_1 := inv_fun inh_Ord B (image B g) g.
Lemma g_1_bij : fun_bijection (image B g) B g_1.
#[local] Hint Resolve g_1_bij : schutte.
Lemma g_1_of : ordering_function g_1 (image B g) B.
Lemma image_B_g_seg : ordering_segment (image B g) B.
Corresponds to Lemma 3 of Schutte's chapter :
It is used twice in the building of ordering function for any subset B of ordinal
For any set B, we build by transfinite induction the ordering segment of
B and the (unique upto extensionnality) ordering function of B
Section building_ordering_function_by_induction.
Variable B : Ensemble Ord.
Lemma ordering_segments_of_B (beta : Ord) :
In B beta →
∃! A : Ensemble Ord,
ordering_segment A (proper_segment_of B beta).
Theorem ordering_segment_ex_unique : ∃! S, ordering_segment S B.
Theorem ordering_function_ex : ∃ ! S, ∃ f, ordering_function f S B.
Lemma ord_ok :
ordering_function (ord B) (the_ordering_segment B) B.
Lemma segment_the_ordering_segment :
segment (the_ordering_segment B).
Lemma ord_eq (A : Ensemble Ord) (f : Ord → Ord) :
ordering_function f A B →
fun_equiv f (ord B) A (the_ordering_segment B).
End building_ordering_function_by_induction.
About ordering_function_ex.
About ordering_function_unicity.
Lemma of_image : ∀ f A B, ordering_function f A B →
ordering_function f A (image A f).
Section Th13_5.
Variables (A B : Ensemble Ord).
Variable f : Ord → Ord.
Hypothesis f_ord : ordering_function f A B.
Section recto.
Hypothesis f_cont : continuous f A B.
Lemma Th_13_5_1 : Closed B.
End recto.
Section verso.
Hypothesis B_closed : Closed B.
Lemma Th_13_5_2 : continuous f A B.
End verso.
End Th13_5.
Theorem TH_13_6 (B : Ensemble Ord)(f : Ord → Ord) :
normal f B → Closed B ∧ Unbounded B.
Lemma ordering_unbounded_unbounded :
∀ A B f, ordering_function f A B →
(Unbounded B ↔ Unbounded A).
Theorem TH_13_6R (A B : Ensemble Ord) (f : Ord → Ord) :
ordering_function f A B →
Closed B → Unbounded B → normal f B.
If f is the ordering function of B, then f 0 is the least element of
B
Lemma ordering_function_least_least :
∀ B f , ordering_function f ordinal B →
least_member lt B (f zero).
Lemma segment_lt_closed : ∀ A a b, segment A →
In A b →
a < b →
In A a.
Lemma th_In A alpha : In (the_ordering_segment A) alpha →
In A (ord A alpha).
About Th_13_5_2.
Arguments ord : clear implicits.
Arguments the_ordering_segment : clear implicits.