Grace/Cumulus/Set/WellOrder.g17

Open in Workbench Download source

Imports

Order

Declarations

Source

1-- Well-orders: least elements, initial segments below a point, restriction2-- to a subset, and the rigidity of order embeddings3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Set.WellOrder9import Order1011-- The initial segment of A below a.12def segment (A r a : Set) : Set := { x ∈ A | relates(r, x, a) }1314-- The order r restricted to the subset B.15def restrictOrder (r B : Set) : Set := r ∩ (B × B)1617theorem segment.subset (A r a : Set)18  shows segment(A, r, a) ⊆ A19proof20  intros x hx21  simp [segment.membership] at hx22  exact hx.left2324theorem restrictOrder.relates (r B x y : Set)25  shows relates(restrictOrder(r, B), x, y) ↔ relates(r, x, y) ∧ x ∈ B ∧ y ∈ B26proof27  constructor28  . intro h29    have member : (x, y) ∈ restrictOrder(r, B) := h30    simp [restrictOrder, intersection.membership] at member31    have coordinates := product.pair_membership.forward with member.right32    constructor33    . exact member.left34    . exact coordinates35  . intro h36    have pairIn : (x, y) ∈ B × B := product.pair with h.right.left, h.right.right37    have inR : (x, y) ∈ r := h.left38    have member : (x, y) ∈ restrictOrder(r, B) by simp [restrictOrder, intersection.membership, inR, pairIn]39    exact member4041-- Least elements4243theorem WellOrder.least (A r S : Set)44  requires order : WellOrder(A, r)45  requires hS : S ⊆ A46  requires nonempty : S ≠ ∅47  shows ∃ m ∈ S, ∀ x ∈ S, x ≠ m → relates(r, m, x)48proof49  have founded := WellOrder.well_founded with order50  have bounded : subset(S, A)51    intros x hx52    exact hS with x, hx53  obtain ⟨m, hm, minimal⟩ := founded with S, ⟨bounded, nonempty⟩54  have connected := StrictLinearOrder.connected with (WellOrder.strict_linear with order)55  witness m56  constructor57  . exact hm58  . intros x hx different59    have differentBack : m ≠ x60      intro same61      apply different62      rw same63      rfl64    have cases := connected with m, (hS with m, hm), x, (hS with x, hx), differentBack65    cases cases with below | above66    . exact below67    . exfalso68      exact minimal with x, hx, above6970theorem WellOrder.least_unique (A r S m n : Set)71  requires order : WellOrder(A, r)72  requires hS : S ⊆ A73  requires hm : m ∈ S74  requires hn : n ∈ S75  requires leastM : ∀ x ∈ S, x ≠ m → relates(r, m, x)76  requires leastN : ∀ x ∈ S, x ≠ n → relates(r, n, x)77  shows m = n78proof79  by_contra different80  have differentBack : n ≠ m81    intro same82    apply different83    rw same84    rfl85  have below := leastM with n, hn, differentBack86  have above := leastN with m, hm, different87  have irreflexive := StrictLinearOrder.irreflexive with (WellOrder.strict_linear with order)88  have transitive := StrictLinearOrder.transitive with (WellOrder.strict_linear with order)89  have loop := transitive with m, (hS with m, hm), n, (hS with n, hn), m, (hS with m, hm), below, above90  exact irreflexive with m, (hS with m, hm), loop9192-- Initial segments below a point9394theorem segment.initial (A r a : Set)95  requires order : StrictOrder(A, r)96  requires ha : a ∈ A97  shows InitialSegment(A, r, segment(A, r, a))98proof99  have transitive := StrictOrder.transitive with order100  constructor101  . exact segment.subset at A, r, a102  . intros x hx y hy below103    simp [segment.membership] at hx104    simp [segment.membership]105    constructor106    . exact hy107    . exact transitive with y, hy, x, hx.left, a, ha, below, hx.right108109theorem segment.absent (A r a : Set)110  requires order : StrictOrder(A, r)111  requires ha : a ∈ A112  shows ¬(a ∈ segment(A, r, a))113proof114  intro h115  simp [segment.membership] at h116  have irreflexive := StrictOrder.irreflexive with order117  exact irreflexive with a, ha, h.right118119theorem segment.proper (A r a : Set)120  requires order : StrictOrder(A, r)121  requires ha : a ∈ A122  shows ProperInitialSegment(A, r, segment(A, r, a))123proof124  constructor125  . exact segment.initial with order, ha126  . intro equal127    have absent := segment.absent with order, ha128    rw equal at absent129    exact absent with ha130131theorem segment.monotone (A r a b : Set)132  requires order : StrictOrder(A, r)133  requires ha : a ∈ A134  requires hb : b ∈ A135  requires below : relates(r, a, b)136  shows segment(A, r, a) ⊆ segment(A, r, b)137proof138  have transitive := StrictOrder.transitive with order139  intros x hx140  simp [segment.membership] at hx141  simp [segment.membership]142  constructor143  . exact hx.left144  . exact transitive with x, hx.left, a, ha, b, hb, hx.right, below145146theorem segment.injective (A r a b : Set)147  requires order : StrictLinearOrder(A, r)148  requires ha : a ∈ A149  requires hb : b ∈ A150  requires equal : segment(A, r, a) = segment(A, r, b)151  shows a = b152proof153  by_contra different154  have connected := StrictLinearOrder.connected with order155  have strict := StrictLinearOrder.strict with order156  have cases := connected with a, ha, b, hb, different157  cases cases with below | above158  . have member : a ∈ segment(A, r, b) by simp [segment.membership, ha, below]159    rw ← equal at member160    exact segment.absent with strict, ha, member161  . have member : b ∈ segment(A, r, a) by simp [segment.membership, hb, above]162    rw equal at member163    exact segment.absent with strict, hb, member164165theorem InitialSegment.cases (A r I : Set)166  requires order : WellOrder(A, r)167  requires initial : InitialSegment(A, r, I)168  shows I = A ∨ ∃ a ∈ A, I = segment(A, r, a)169proof170  have included := InitialSegment.subset with initial171  have strict := StrictLinearOrder.strict with (WellOrder.strict_linear with order)172  have connected := StrictLinearOrder.connected with (WellOrder.strict_linear with order)173  have irreflexive := StrictOrder.irreflexive with strict174  have split : I = A ∨ I ≠ A by tauto175  cases split with whole | proper176  . left177    exact whole178  . right179    have outside : A ∖ I ≠ ∅180      intro empty181      apply proper182      apply Subset.antisymmetric183      . exact included184      . exact difference.eq_empty_iff.forward with empty185    obtain ⟨a, haOut, leastA⟩ := WellOrder.least with order, (difference.subset_left at A, I), outside186    simp [difference.membership] at haOut187    witness a188    constructor189    . exact haOut.left190    . ext x191      constructor192      . intro hx193        have hxA : x ∈ A := included with x, hx194        simp [segment.membership]195        constructor196        . exact hxA197        . have different : x ≠ a198            intro same199            rw same at hx200            exact haOut.right with hx201          have cases := connected with x, hxA, a, haOut.left, different202          cases cases with below | above203          . exact below204          . exfalso205            exact haOut.right with (initial.right with x, hx, a, haOut.left, above)206      . intro hx207        simp [segment.membership] at hx208        by_contra absent209        have inOutside : x ∈ A ∖ I by simp [difference.membership, hx.left, absent]210        have different : x ≠ a211          intro same212          rw same at hx213          exact irreflexive with a, haOut.left, hx.right214        have above := leastA with x, inOutside, different215        have transitive := StrictOrder.transitive with strict216        have loop := transitive with x, hx.left, a, haOut.left, x, hx.left, hx.right, above217        exact irreflexive with x, hx.left, loop218219-- Restriction to a subset220221theorem restrictOrder.relation (r B : Set)222  shows RelationBetween(restrictOrder(r, B), B, B)223proof224  intros p hp225  simp [restrictOrder, intersection.membership] at hp226  exact hp.right227228theorem restrictOrder.well_order (A r B : Set)229  requires order : WellOrder(A, r)230  requires hB : B ⊆ A231  shows WellOrder(B, restrictOrder(r, B))232proof233  have strict := StrictLinearOrder.strict with (WellOrder.strict_linear with order)234  have connected := StrictLinearOrder.connected with (WellOrder.strict_linear with order)235  have irreflexive := StrictOrder.irreflexive with strict236  have transitive := StrictOrder.transitive with strict237  constructor238  . constructor239    . constructor240      . exact restrictOrder.relation at r, B241      . constructor242        . intros x hx loop243          have related := restrictOrder.relates.forward with loop244          exact irreflexive with x, (hB with x, hx), related.left245        . intros x hx y hy z hz first second246          have firstR := restrictOrder.relates.forward with first247          have secondR := restrictOrder.relates.forward with second248          apply restrictOrder.relates.backward249          constructor250          . exact transitive with x, (hB with x, hx), y, (hB with y, hy), z, (hB with z, hz), firstR.left, secondR.left251          . exact ⟨hx, hz⟩252    . intros x hx y hy different253      have cases := connected with x, (hB with x, hx), y, (hB with y, hy), different254      cases cases with below | above255      . left256        apply restrictOrder.relates.backward257        exact ⟨below, hx, hy⟩258      . right259        apply restrictOrder.relates.backward260        exact ⟨above, hy, hx⟩261  . intros S hS262    have included : S ⊆ A263      intros x hx264      exact hB with x, (hS.left with x, hx)265    obtain ⟨m, hm, leastM⟩ := WellOrder.least with order, included, hS.right266    witness m267    constructor268    . exact hm269    . intros y hy below270      have related := restrictOrder.relates.forward with below271      have different : y ≠ m272        intro same273        rw same at related274        exact irreflexive with m, (included with m, hm), related.left275      have above := leastM with y, hy, different276      have loop := transitive with m, (included with m, hm), y, (included with y, hy), m, (included with m, hm), above, related.left277      exact irreflexive with m, (included with m, hm), loop278279-- Rigidity of embeddings280281-- The points an embedding moves down.282def descents (f A r : Set) : Set := { x ∈ A | relates(r, f(x), x) }283284theorem OrderEmbedding.not_below (f A r : Set)285  requires order : WellOrder(A, r)286  requires embedding : OrderEmbedding(f, A, r, A, r)287  shows ∀ x ∈ A, ¬(relates(r, f(x), x))288proof289  have function := Injective.function with embedding.left290  have strict := StrictLinearOrder.strict with (WellOrder.strict_linear with order)291  have irreflexive := StrictOrder.irreflexive with strict292  by_contra some293  have descending : descents(f, A, r) ≠ ∅294    intro empty295    apply some296    intros x hx below297    have member : x ∈ descents(f, A, r) by simp [descents.membership, hx, below]298    rw empty at member299    exact set.empty with member300  have descendingSubset : descents(f, A, r) ⊆ A301    intros x hx302    simp [descents.membership] at hx303    exact hx.left304  obtain ⟨m, hm, leastM⟩ := WellOrder.least with order, descendingSubset, descending305  simp [descents.membership] at hm306  have valueA := FunctionBetween.apply_closed with function, hm.left307  have related := FunctionBetween.relates_apply with function, hm.left308  have relatedValue := FunctionBetween.relates_apply with function, valueA309  have preserved := embedding.right with f(m), valueA, m, hm.left, f(f(m)), (FunctionBetween.apply_closed with function, valueA), f(m), valueA, relatedValue, related310  have lower := preserved.forward with hm.right311  have inDescending : f(m) ∈ descents(f, A, r) by simp [descents.membership, valueA, lower]312  have different : f(m) ≠ m313    intro same314    rw same at hm315    exact irreflexive with m, hm.left, hm.right316  have above := leastM with f(m), inDescending, different317  have transitive := StrictOrder.transitive with strict318  have loop := transitive with m, hm.left, f(m), valueA, m, hm.left, above, hm.right319  exact irreflexive with m, hm.left, loop320