Grace/Cumulus/Real/Order.g17

Open in Workbench Download source

Imports

Core

Declarations

Source

1-- Order completeness of the Dedekind reals2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Real.Order8import Core910-- Non-strict order on lower cuts is inclusion. Keeping it proposition-valued11-- makes the mathematical content visible while the graph interface matures.12predicate RealLe (A B : Set) := Real(A) ∧ Real(B) ∧ (A ⊆ B)1314-- Non-strict real order as a set-valued relation graph.  Its15-- proposition-level view remains RealLe; the graph supports typed ≤ notation16-- and the same inspectable elaboration boundary as realLess.17def realLe : Set :=18  { p ∈ ℝ × ℝ | ∃ A ∈ ℝ, ∃ B ∈ ℝ, p = (A, B) ∧ (A ⊆ B) }1920theorem realLe.characterization (A B : Set)21  shows relates(realLe, A, B) ↔ RealLe(A, B)22proof23  constructor24  . intro le25    unfold relates at le26    simp [realLe.membership] at le27    rcases le with ⟨_, X, realX, Y, realY, pairShape, subset⟩28    obtain ⟨equalA, equalB⟩ := orderedPair.injective with pairShape29    constructor30    . unfold Real31      rwa equalA32    . constructor33      . unfold Real34        rwa equalB35      . rw [equalA, equalB]36        exact subset37  . intro le38    rcases le with ⟨realA, realB, subset⟩39    unfold relates40    apply realLe.membership.backward41    constructor42    . apply product.pair at A, B, ℝ, ℝ43        exact realA44        exact realB45    . witness A46      constructor47        exact realA48      . witness B49        constructor50          exact realB51        refine ⟨rfl, subset⟩5253theorem realLe.relation54  shows RelationBetween(realLe, ℝ, ℝ)55proof56  intros p hp57  obtain ⟨bounded, witnesses⟩ := realLe.membership.forward with hp58  exact bounded5960instance realLe.operation61  shows LessEqualOperation(ℝ, realLe)62proof63  exact realLe.relation6465notation infix 50 "≤" => relates via LessEqualOperation(ℝ, _) for Real6667theorem realLe.subset (A B : Real)68  requires le : A ≤ B69  shows A ⊆ B70proof71  have proposition := realLe.characterization.forward with le72  unfold RealLe at proposition73  simp7475theorem realLe.of_subset (A B : Real)76  requires subset : A ⊆ B77  shows A ≤ B78proof79  apply realLe.characterization.backward80  unfold RealLe81  tauto8283predicate RealUpperBound (S B : Set) :=84  Real(B) ∧ (S ⊆ ℝ) ∧ (∀ A ∈ S, (A ⊆ B))8586predicate RealLeastUpperBound (S U : Set) :=87  RealUpperBound(S, U) ∧88  (∀ B, RealUpperBound(S, B) → (U ⊆ B))8990-- The union of a family of lower cuts is its candidate supremum.91def realSup (S : Set) : Set := ⋃(S)9293theorem RealLe.reflexive (A : Set)94  requires realA : Real(A)95  shows RealLe(A, A)96proof97  refine ⟨realA, realA, Subset.reflexive at A⟩9899theorem RealLe.transitive (A B C : Set)100  requires hAB : RealLe(A, B)101  requires hBC : RealLe(B, C)102  shows RealLe(A, C)103proof104  rcases hAB with ⟨realA, realB, subsetAB⟩105  rcases hBC with ⟨realBAgain, realC, subsetBC⟩106  constructor107  exact realA108  constructor109  exact realC110  exact Subset.transitive with subsetAB, subsetBC111112theorem RealLe.antisymmetric (A B : Set)113  requires hAB : RealLe(A, B)114  requires hBA : RealLe(B, A)115  shows A = B116proof117  rcases hAB with ⟨realA, realB, subsetAB⟩118  rcases hBA with ⟨realBAgain, realAAgain, subsetBA⟩119  exact Subset.antisymmetric with subsetAB, subsetBA120121theorem realSup.subset_upper (S B : Set)122  requires upper : RealUpperBound(S, B)123  shows (realSup(S) ⊆ B)124proof125  rcases upper with ⟨realB, reals, bounds⟩126  unfold realSup127  exact union.subset with bounds128129theorem realSup.cut (S B : Set)130  requires inhabited : Nonempty(S)131  requires upper : RealUpperBound(S, B)132  shows DedekindCut(realSup(S))133proof134  rcases upper with ⟨realB, reals, bounds⟩135  have cutB := Real.characterization.forward with realB136  constructor137    intros q0 hq0138    unfold realSup at hq0139    simp [set.union] at hq0140    obtain ⟨A, hAS, hq0A⟩ := hq0141    specialize reals with A, hAS142    obtain ⟨powerA, cutA⟩ := Grace.Cumulus.Real.Defs.reals.membership.forward with reals143    have subsetA := DedekindCut.subset_rationals with cutA144    exact subsetA with q0, hq0A145  . constructor146    . obtain ⟨A0, hA0S⟩ := inhabited147      specialize reals with A0, hA0S148      obtain ⟨powerA, cutA⟩ := Grace.Cumulus.Real.Defs.reals.membership.forward with reals149      obtain ⟨q1, hq1A⟩ := DedekindCut.nonempty with cutA150      witness q1151      unfold realSup152      exact union.contains with hA0S, hq1A153    . constructor154      . intro equalQ155        unfold realSup at equalQ156        have unionBound := union.subset with bounds157        rw equalQ at unionBound158        have subsetB := DedekindCut.subset_rationals with cutB159        have equalB := Subset.antisymmetric with subsetB, unionBound160        have properB := DedekindCut.proper with cutB161        exact ProperSubset.ne with properB, equalB162      . constructor163        . intros q2 hq2 p2 hp2 less2164          unfold realSup at hq2165          simp [set.union] at hq2166          obtain ⟨A1, hA1S, hq2A1⟩ := hq2167          specialize reals with A1, hA1S168          obtain ⟨powerA, cutA⟩ := Grace.Cumulus.Real.Defs.reals.membership.forward with reals169          have downward := DedekindCut.downward with cutA, hq2A1, hp2, less2170          unfold realSup171          exact union.contains with hA1S, downward172        . intros q3 hq3173          unfold realSup at hq3174          simp [set.union] at hq3175          obtain ⟨A2, hA2S, hq3A2⟩ := hq3176          specialize reals with A2, hA2S177          obtain ⟨powerA, cutA⟩ := Grace.Cumulus.Real.Defs.reals.membership.forward with reals178          obtain ⟨r3, hr3A2, less3⟩ := DedekindCut.no_greatest with cutA, hq3A2179          witness r3180          constructor181          . unfold realSup182            exact union.contains with hA2S, hr3A2183          . exact less3184185theorem realSup.least_upper_bound (S B : Set)186  requires inhabited : Nonempty(S)187  requires upper : RealUpperBound(S, B)188  shows RealLeastUpperBound(S, realSup(S))189proof190  constructor191    constructor192    . apply Real.characterization.backward at realSup(S)193      exact realSup.cut with inhabited, upper194    . rcases upper with ⟨realB, reals, bounds⟩195      constructor196      . exact reals197      . intros A hAS q hqA198        unfold realSup199        exact union.contains with hAS, hqA200  . intros C upperC201    exact realSup.subset_upper with upperC202203-- Every inhabited family of reals with a real upper bound has a least one.204-- This is the least-upper-bound property used by real analysis.205theorem Real.least_upper_bound_property (S : Set)206  requires inhabited : Nonempty(S)207  requires bounded : ∃ B, RealUpperBound(S, B)208  shows ∃ U, RealLeastUpperBound(S, U)209proof210  obtain ⟨B, upper⟩ := bounded211  witness realSup(S)212  exact realSup.least_upper_bound with inhabited, upper213