Grace/Cumulus/Topology/HeineBorel.g17

Open in Workbench Download source

Imports

Real · Real.Analysis.SequentialCompactness

Declarations

Source

1-- Heine–Borel on the line: a closed interval is compact. The points of2-- [A, B] up to which finitely many members of an open cover suffice have a3-- supremum, and the cover member around that supremum pushes it to B.4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Topology.HeineBorel10import Real11import Real.Analysis.SequentialCompactness1213theorem dist.lt_of_bounds (X U E : Real)14  requires lower : U - E < X15  requires upper : X < U + E16  shows dist(X, U) < E17proof18  unfold dist19  have order := realLess.trichotomy at X - U, (0:R)20  cases order with negative | rest21  . have nonpositive := realLess.implies_le with negative22    have value := abs.of_nonpositive with nonpositive23    rw value24    linarith25  . cases rest with zero | positive26    . rw [zero, abs.zero]27      linarith28    . have nonnegative := realLess.implies_le with positive29      have value := abs.of_nonnegative with nonnegative30      rw value31      linarith3233theorem closedInterval.singleton_subset (A : Real) (U : Set)34  requires hA : A ∈ U35  shows closedInterval(A, A) ⊆ U36proof37  intros x hx38  obtain ⟨realX, lower, upper⟩ := closedInterval.membership.forward with hx39  have same := realLe.antisymmetric with upper, lower40  rwa same4142-- The points x of [A, B] such that [A, x] is covered by finitely many43-- members of C.44def coveredBelow (C : Set, A B : Real) : Set :=45  { x ∈ closedInterval(A, B) | ∃ F, F ⊆ C ∧ Finite(F) ∧ closedInterval(A, x) ⊆ ⋃(F) }4647theorem closedInterval.compact (A B : Real)48  requires ordered : A ≤ B49  shows IsCompact(ℝ, realTopology, closedInterval(A, B))50proof51  constructor52  . exact closedInterval.subset_reals at A, B53  . intros C cover54    obtain ⟨coverOpen, covers⟩ := cover55    have leftIn := closedInterval.left_mem with ordered56    obtain ⟨W0, hW0, hAW0⟩ := union.membership.forward with (covers with A, leftIn)57    have startMember : A ∈ coveredBelow(C, A, B)58      apply coveredBelow.membership.backward59      refine ⟨leftIn, {W0}, ?_, (Finite.singleton at W0), ?_⟩60      . intros V hV61        have same := singleton.membership.forward with hV62        rwa same63      . rw union.singleton64        exact closedInterval.singleton_subset with hAW065    have inhabited : Nonempty(coveredBelow(C, A, B)) := ⟨A, startMember⟩66    have subsetInterval : coveredBelow(C, A, B) ⊆ closedInterval(A, B)67      intros x hx68      have parts := coveredBelow.membership.forward with hx69      exact parts.left70    have subsetReals := Subset.transitive with subsetInterval, (closedInterval.subset_reals at A, B)71    have realB : Real(B) by typecheck72    have upperB : RealUpperBound(coveredBelow(C, A, B), B)73      refine ⟨realB, subsetReals, ?_⟩74      intros x hx75      obtain ⟨realX, lower, upper⟩ := closedInterval.membership.forward with (subsetInterval with x, hx)76      exact realLe.subset with upper77    have bounded : ∃ D, RealUpperBound(coveredBelow(C, A, B), D) := ⟨B, upperB⟩78    obtain ⟨U, least⟩ := Real.least_upper_bound_property with inhabited, bounded79    have upperU := least.left80    have minimal := least.right81    obtain ⟨realU, inReals, bounds⟩ := upperU82    have aBelow := realLe.of_subset with (bounds with A, startMember)83    have uBelow := realLe.of_subset with (minimal with B, upperB)84    have realU2 : U ∈ ℝ by simp [Real]85    have uIn : U ∈ closedInterval(A, B)86      apply closedInterval.membership.backward87      exact ⟨realU2, aBelow, uBelow⟩88    obtain ⟨W, hW, hUW⟩ := union.membership.forward with (covers with U, uIn)89    have partsW := realTopology.membership.forward with (coverOpen with W, hW)90    obtain ⟨E, hE, positive, ballInside⟩ := partsW.right with U, hUW91    obtain ⟨s, hs, near⟩ := RealLeastUpperBound.approached with least, positive92    obtain ⟨sIn, F, hF, finiteF, coveredS⟩ := coveredBelow.membership.forward with hs93    obtain ⟨realS, aS, sB⟩ := closedInterval.membership.forward with sIn94    have sBelowU := realLe.of_subset with (bounds with s, hs)95    have extendedSubset : insert(W, F) ⊆ C96      intros V hV97      have split := insert.membership.forward with hV98      cases split with isW | inF99      . rw isW100        exact hW101      . exact hF with V, inF102    have extendedFinite := Finite.insert at F, W with finiteF103    have memberW : W ∈ insert(W, F)104      apply insert.membership.backward105      left106      rfl107    have halfPositive := half.positive with positive108    have halfSmall := half.lt_self with positive109    have extendedCovers : ∀ t ∈ ℝ, t < U + E → closedInterval(A, t) ⊆ ⋃(insert(W, F))110      intros t realT tBound x hx111      obtain ⟨realX, aX, xT⟩ := closedInterval.membership.forward with hx112      have split := realLess.trichotomy at s, x113      have viaW : (s:R) < (x:R) → x ∈ ⋃(insert(W, F))114        intro below115        have lowerX : U - E < x by linarith116        have upperX : x < U + E by linarith117        have close := dist.lt_of_bounds with lowerX, upperX118        have inBall : x ∈ openBall(U, E) := openBall.membership.backward with ⟨realX, close⟩119        exact union.contains with memberW, (ballInside with x, inBall)120      cases split with below | rest121      . exact viaW with below122      . have xBelowS : x ≤ s123          cases rest with equal | above124          . rw equal125            exact realLe.reflexive126          . exact realLess.implies_le with above127        have inLeft : x ∈ closedInterval(A, s)128          apply closedInterval.membership.backward129          exact ⟨realX, aX, xBelowS⟩130        obtain ⟨V, hV, hxV⟩ := union.membership.forward with (coveredS with x, inLeft)131        have memberV : V ∈ insert(W, F)132          apply insert.membership.backward133          right134          exact hV135        exact union.contains with memberV, hxV136    have split := realLess.trichotomy at B, U + half(E)137    have finish : B < U + E → ∃ G, G ⊆ C ∧ Finite(G) ∧ closedInterval(A, B) ⊆ ⋃(G)138      intro bound139      witness insert(W, F)140      exact ⟨extendedSubset, extendedFinite, (extendedCovers with B, bound)⟩141    cases split with smaller | rest142    . have bound : B < U + E by linarith143      exact finish with bound144    . cases rest with equal | larger145      . have bound : B < U + E by linarith146        exact finish with bound147      . exfalso148        have realT : U + half(E) ∈ ℝ by typecheck149        have tBound : U + half(E) < U + E by linarith150        have tIn : U + half(E) ∈ closedInterval(A, B)151          apply closedInterval.membership.backward152          refine ⟨realT, ?_, (realLess.implies_le with larger)⟩153          linarith154        have tMember : U + half(E) ∈ coveredBelow(C, A, B)155          exact coveredBelow.membership.backward with ⟨tIn, insert(W, F), extendedSubset, extendedFinite, (extendedCovers with U + half(E), tBound)⟩156        have tBelow := realLe.of_subset with (bounds with U + half(E), tMember)157        linarith158