Grace/Cumulus/Set/WellOrdering.g17

Open in Workbench Download source

Imports

Cardinal.Hartogs · ChoiceFunctions · OrderTransport

Declarations

Source

1-- The well-ordering theorem: every set carries a well-order. A choice2-- function enumerates the set along the Hartogs bound, picking at each stage3-- an element not yet chosen; Hartogs' theorem forces the enumeration to4-- exhaust the set at some stage, and the least such stage is an ordinal in5-- bijection with the set, whose membership order transports back.6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Set.WellOrdering12import Cardinal.Hartogs13import ChoiceFunctions14import OrderTransport1516theorem enumerationStep.well_founded (A H c : Set)17  shows wellFoundedOn(membershipOn(H), H)18proof19  simp [membershipOn.wellFounded]2021-- At stage x choose an element of A not chosen at any earlier stage.22noncomputable well-founded def enumerationStep (A H c x : Set) : Set23  over H ordered by membershipOn(H)24  certified by enumerationStep.well_founded25  | x using history => c[A ∖ Relation.range(history)]2627def enumerated (A H c x : Set) : Set :=28  Relation.range(enumerationStep.history(A, H, c, x))2930theorem enumerated.membership (z A H c x : Set)31  shows z ∈ enumerated(A, H, c, x) ↔32    ∃ y ∈ H, relates(membershipOn(H), y, x) ∧ z = enumerationStep(A, H, c, y)33proof34  constructor35  . intro member36    unfold enumerated at member37    obtain ⟨bounded, source, pair⟩ := Relation.range.membership.forward with member38    obtain ⟨y, hy, earlier, equal⟩ := enumerationStep.history.membership.forward with pair39    obtain ⟨sameSource, sameValue⟩ := orderedPair.injective with equal40    refine ⟨y, hy, earlier, sameValue⟩41  . intro represented42    obtain ⟨y, hy, earlier, value⟩ := represented43    have pair : (y, enumerationStep(A, H, c, y)) ∈ enumerationStep.history(A, H, c, x)44      exact enumerationStep.history.membership.backward with ⟨y, hy, earlier, rfl⟩45    have rangeMember := Relation.range.contains with pair46    unfold enumerated47    rwa value4849theorem enumerationStep.selects (A H c x : Set)50  requires hx : x ∈ H51  shows enumerationStep(A, H, c, x) = c[A ∖ enumerated(A, H, c, x)]52proof53  have equation := enumerationStep.equation.direct at A, H, c, x with hx54  simpa [enumerated] using equation5556-- A stage is exhausted when every element of A was chosen before it.57predicate Exhausted (A H c x : Set) := A ⊆ enumerated(A, H, c, x)5859theorem enumerationStep.fresh (A H c x : Set)60  requires choice : SubsetChoice(c, A)61  requires hx : x ∈ H62  requires remaining : ¬Exhausted(A, H, c, x)63  shows enumerationStep(A, H, c, x) ∈ A ∧64    ¬enumerationStep(A, H, c, x) ∈ enumerated(A, H, c, x)65proof66  have inhabited : Nonempty(A ∖ enumerated(A, H, c, x))67    by_contra absent68    apply remaining69    unfold Exhausted70    intros a ha71    by_contra outside72    apply absent73    witness a74    exact difference.membership.backward with ⟨ha, outside⟩75  have subset := difference.subset_left at A, enumerated(A, H, c, x)76  have selected := SubsetChoice.member with choice, subset, inhabited77  have equation := enumerationStep.selects at A, H, c, x with hx78  rw ← equation at selected79  exact difference.membership.forward with selected8081theorem enumerationStep.distinct (A H c x y : Set)82  requires choice : SubsetChoice(c, A)83  requires hx : x ∈ H84  requires hy : y ∈ H85  requires earlier : x ∈ y86  requires remaining : ¬Exhausted(A, H, c, y)87  shows enumerationStep(A, H, c, x) ≠ enumerationStep(A, H, c, y)88proof89  obtain ⟨closed, outside⟩ := enumerationStep.fresh with choice, hy, remaining90  have rule := membershipOn.relates with hx, hy91  have related := rule.backward with earlier92  have prior : enumerationStep(A, H, c, x) ∈ enumerated(A, H, c, y)93    exact enumerated.membership.backward with ⟨x, hx, related, rfl⟩94  intro equal95  rw equal at prior96  exact outside with prior9798-- The enumeration as a function on a set of unexhausted stages.99defgraph enumeration (A H c D : Set) (x ∈ D) : A := enumerationStep(A, H, c, x)100requires choice : SubsetChoice(c, A)101requires stages : D ⊆ H102requires remaining : ∀ x ∈ D, ¬Exhausted(A, H, c, x)103proof104  have hxH := stages with x, assumption105  have unexhausted := remaining with x, assumption106  obtain ⟨closed, outside⟩ := enumerationStep.fresh with choice, hxH, unexhausted107  exact closed108109theorem enumeration.injective (A H c D : Set)110  requires ordinal : H ∈ Ordinal111  requires choice : SubsetChoice(c, A)112  requires stages : D ⊆ H113  requires remaining : ∀ x ∈ D, ¬Exhausted(A, H, c, x)114  shows InjectiveBetween(enumeration(A, H, c, D), D, A)115proof116  have function := enumeration.function at A, H, c, D with *117  constructor118  . exact function119  . intros x hx y hy z hz mappedX mappedY120    have valueX := FunctionBetween.apply_value with function, hx, mappedX121    have valueY := FunctionBetween.apply_value with function, hy, mappedY122    have stepX := enumeration.value at A, H, c, D, x with *123    have stepY := enumeration.value at A, H, c, D, y with *124    have equalValues : enumerationStep(A, H, c, x) = enumerationStep(A, H, c, y) by cc125    have hxH := stages with x, hx126    have hyH := stages with y, hy127    have xOrdinal := Ordinal.member with ordinal, hxH128    have yOrdinal := Ordinal.member with ordinal, hyH129    have alternatives := Ordinal.trichotomy with xOrdinal, y, yOrdinal130    cases alternatives with xy | rest131    . exfalso132      have distinct := enumerationStep.distinct with choice, hxH, hyH, xy, (remaining with y, hy)133      exact distinct with equalValues134    . cases rest with equal | yx135      . exact equal136      . exfalso137        have distinct := enumerationStep.distinct with choice, hyH, hxH, yx, (remaining with x, hx)138        apply distinct139        symm140        exact equalValues141142-- Hartogs' theorem: some stage below the Hartogs bound exhausts A.143theorem enumeration.exhausts (A c : Set)144  requires choice : SubsetChoice(c, A)145  shows ∃ x ∈ hartogsBound(A), Exhausted(A, hartogsBound(A), c, x)146proof147  by_contra none148  have remaining : ∀ x ∈ hartogsBound(A), ¬Exhausted(A, hartogsBound(A), c, x)149    intros x hx exhausted150    apply none151    refine ⟨x, hx, exhausted⟩152  have ordinal := hartogsBound.ordinal at A153  have stages := Subset.reflexive at hartogsBound(A)154  have injection := enumeration.injective with *155  exact hartogsBound.no_injection with injection156157def exhaustedStages (A H c : Set) : Set := {x ∈ H | Exhausted(A, H, c, x)}158159theorem enumeration.least_exhausted (A c : Set)160  requires choice : SubsetChoice(c, A)161  shows ∃ m ∈ hartogsBound(A), Exhausted(A, hartogsBound(A), c, m) ∧162    (∀ x ∈ m, ¬Exhausted(A, hartogsBound(A), c, x))163proof164  have ordinal := hartogsBound.ordinal at A165  obtain ⟨x, hx, exhausted⟩ := enumeration.exhausts with choice166  have ordinals : ∀ α ∈ exhaustedStages(A, hartogsBound(A), c), α ∈ Ordinal167    intros α hα168    have parts := exhaustedStages.membership.forward with hα169    exact Ordinal.member with ordinal, parts.left170  have member : x ∈ exhaustedStages(A, hartogsBound(A), c)171    exact exhaustedStages.membership.backward with ⟨hx, exhausted⟩172  have nonempty := Nonempty.ne_empty at exhaustedStages(A, hartogsBound(A), c) with ⟨x, member⟩173  obtain ⟨m, hm, least⟩ := Ordinal.least with ordinals, nonempty174  have parts := exhaustedStages.membership.forward with hm175  refine ⟨m, parts.left, parts.right, ?_⟩176  intros y hy exhaustedY177  have below := Ordinal.member_subset with ordinal, parts.left178  have memberY : y ∈ exhaustedStages(A, hartogsBound(A), c)179    exact exhaustedStages.membership.backward with ⟨(below with y, hy), exhaustedY⟩180  have bound := least with y, memberY181  have loop := bound with y, hy182  have irreflexive := Ordinal.not_member_self at y183  exact irreflexive with loop184185theorem enumeration.surjective (A H c D : Set)186  requires ordinal : H ∈ Ordinal187  requires choice : SubsetChoice(c, A)188  requires stage : D ∈ H189  requires exhausted : Exhausted(A, H, c, D)190  requires remaining : ∀ x ∈ D, ¬Exhausted(A, H, c, x)191  shows SurjectiveBetween(enumeration(A, H, c, D), D, A)192proof193  have stages := Ordinal.member_subset with ordinal, stage194  have function := enumeration.function at A, H, c, D with *195  constructor196  . exact function197  . intros a ha198    unfold Exhausted at exhausted199    have covered := exhausted with a, ha200    obtain ⟨y, hy, related, value⟩ := enumerated.membership.forward with covered201    have rule := membershipOn.relates with hy, stage202    have hyD := rule.forward with related203    refine ⟨y, hyD, ?_⟩204    have step := enumeration.value at A, H, c, D, y with *205    have graph := FunctionBetween.relates_apply with function, hyD206    rwa [step, ← value] at graph207208theorem WellOrder.exists (A : Set)209  shows ∃ r, WellOrder(A, r)210proof211  obtain ⟨c, choice⟩ := SubsetChoice.exists at A212  have ordinal := hartogsBound.ordinal at A213  obtain ⟨m, hm, exhausted, remaining⟩ := enumeration.least_exhausted with choice214  have stages := Ordinal.member_subset with ordinal, hm215  have mOrdinal := Ordinal.member with ordinal, hm216  have injective := enumeration.injective with *217  have surjective := enumeration.surjective with *218  have order := Ordinal.well_order with mOrdinal219  have transported := transportedOrder.well_order with injective, order220  have covering : functionImage(enumeration(A, hartogsBound(A), c, m), m, A) = A221    apply Subset.antisymmetric222    . exact functionImage.subset at enumeration(A, hartogsBound(A), c, m), m, A223    . intros a ha224      obtain ⟨y, hy, related⟩ := surjective.right with a, ha225      have value := FunctionBetween.apply_value with surjective.left, hy, related226      have closed := FunctionBetween.apply_closed with surjective.left, hy227      rw ← value228      simp [functionImage.membership]229  rw covering at transported230  witness transportedOrder(enumeration(A, hartogsBound(A), c, m), m, A, membershipOn(m))231  exact transported232