Section Tower.
Variable (X : ExtType) (eta : set X -> set X).
Implicit Types (p q : set X) (F : set X -> Prop).
Hypothesis eta_ext : forall p x, eta p x -> ~ p x.
Hypothesis eta_uniq : forall p, unique (eta p).
Definition adj p := p :|: eta p.
Inductive Stage : set X -> Prop :=
| StgA p : Stage p -> Stage (adj p)
| StgU F : F <<= Stage -> Stage (Union F).
Lemma eta_full_empty : ~ inhab (eta (Union Stage)).
Lemma compare_union p F :
(forall q, F q -> cmp p q) -> cmp p (Union F).
Lemma compare_adj p q :
p <<= adj q -> q <<= adj p -> cmp (adj p) (adj q).
Theorem linearity : linears Stage.
Hypothesis eta_greedy : forall p, inhab (complement p) -> inhab (eta p).
Lemma adj_fix p : adj p <<= p -> (forall x, p x).
Lemma StgU_full x : Union Stage x.
Lemma StgT : Stage setT.
Lemma sandwich p q : p << q -> q <<= adj p -> adj p <<= q.
Lemma adj_incl p q : Stage p -> Stage q -> p << q -> adj p <<= q.
Lemma tower_least (F : set (set X)) :
F <<= Stage -> inhab F -> F (Inter F).
Inclusion is a well-ordering of Stages
Additional Facts -- only needed for bar_suj below
Lemma eta_fix p : eta p <<= p -> (forall x, ~ eta p x).
Lemma etaN_full p : (forall x, ~ eta p x) -> (forall x, p x).
Lemma eta_ssub_neq p q :
Stage p -> Stage q -> p << q -> eta p <> eta q.
Lemma eta_inj p q :
Stage p -> Stage q -> eta p = eta q -> p = q.
End Tower.
Module Hausdorff.
Section Hausdorff.
Variables (X : ExtChoiceType) (R : X -> X -> Prop).
Implicit Types (p q : set X) (F : set X -> Prop).
Definition chain p := forall x y, p x -> p y -> R x y \/ R y x.
Definition eta p := gamma (fun x => ~ p x /\ chain (setU1 p x)).
Lemma unique_eta p : unique (eta p).
Lemma co_choice_eta p x : eta p x -> ~p x.
Local Notation Stage := (Stage eta).
Lemma linear_Chains : linears Stage.
Lemma ChainsP : Stage <<= chain.
Theorem Hausdorff :
exists M, chain M /\ (forall x, chain (setU1 M x) -> M x).
End Hausdorff.
End Hausdorff.
Export Hausdorff.
Module Zermelo.
Section Zermelo.
Variables (X : ExtChoiceType).
Implicit Types (x : X) (p q : set X).
Definition eta p := gamma (fun x => ~ p x).
Lemma cochoice_eta p x : eta p x -> ~ p x.
Lemma greedy_eta p : inhab (fun x => ~ p x) -> inhab (eta p).
Lemma unique_eta p : unique (eta p).
Local Notation Stage := (Stage eta).
Local Notation adj := (adj eta).
Definition bar x := Union (fun p => Stage p /\ ~ p x).
Lemma stage_bar x : Stage (bar x).
Lemma barN x : ~ bar x x.
Lemma barP x : eta (bar x) = set1 x.
Lemma inj_bar : injective bar.
Definition bar_rel x y := bar x <<= bar y.
Theorem wo_bar_rel : wo_on setT bar_rel.
Lemma bar_sub p x : p x -> Stage p -> bar x <<= p /\ bar x <> p.
Definition Seg R x := fun z => R z x /\ z <> x.
Lemma bar_seg x : bar x = Seg bar_rel x.
Definition agrees R := forall x, gamma (complement (Seg R x)) = set1 x.
Lemma agrees_bar : agrees bar_rel.
Theorem Zermelo : exists2 R, wo_on setT R & agrees R.
Fact bar_suj p : Stage p -> inhab (complement p) -> exists x, p = bar x.
End Zermelo.
Section Extension.
Variables (X : ExtChoiceType) (R : relation X).
Definition min p x := p x /\ (forall y, p y -> R y x -> y = x).
Hypothesis well_founded_R : forall p, inhab p -> inhab (min p).
Build a second ExtChoiceType for sort X whose choice function picks
R-minimal elements
Definition gamma' p := gamma (min p).
Lemma gammaP1' p : gamma' p <<= p.
Lemma gammaP2' p : inhab p -> single (gamma' p).
Definition X' := Build_ExtChoiceType gammaP1' gammaP2'.
For gamma' all stages are downward closed