Grace/Cumulus/Topology/Real/RationalBase.g17

Open in Workbench Download source

Imports

Basis · Rat.Countable

Declarations

• rationalIntervals def
• openInterval.member_intervals theorem derivation
• rationalIntervals.open theorem derivation
• rationalIntervals.basis theorem derivation
• rationalPairs def
• rationalPairs.countable theorem derivation
• rationalInterval defgraph
• rationalInterval.surjective theorem derivation
• rationalIntervals.countable theorem derivation

Source

1-- The rational intervals: open intervals with rational endpoints form a2-- countable basis of the real line, by the density of ℚ in ℝ3-- (Real/Embedding)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.Real.RationalBase10import Basis11import Rat.Countable1213-- The open intervals with rational endpoints.14def rationalIntervals : Set :=15  { W ∈ 𝒫(ℝ) | ∃ p ∈ ℚ, ∃ q ∈ ℚ, p < q ∧16    W = openInterval(rationalCut(p), rationalCut(q)) }1718theorem openInterval.member_intervals (p q : Rational)19  requires less : p < q20  shows openInterval(rationalCut(p), rationalCut(q)) ∈ rationalIntervals21proof22  have realP := rationalCut.real at p with assumption23  have realQ := rationalCut.real at q with assumption24  have pInQ : p ∈ ℚ by typecheck25  have qInQ : q ∈ ℚ by typecheck26  apply rationalIntervals.membership.backward27  refine ⟨?_, p, pInQ, q, qInQ, less, rfl⟩28  apply powerset.membership_iff.backward29  exact openInterval.subset_reals at rationalCut(p), rationalCut(q)3031theorem rationalIntervals.open32  shows rationalIntervals ⊆ realTopology33proof34  intros W hW35  have parts := rationalIntervals.membership.forward with hW36  obtain ⟨p, hp, q, hq, less, shape⟩ := parts.right37  have realP := rationalCut.real at p with hp38  have realQ := rationalCut.real at q with hq39  rw shape40  exact openInterval.open at rationalCut(p), rationalCut(q)4142-- Every open set around a real contains a rational interval around it.43theorem rationalIntervals.basis44  shows Basis(ℝ, realTopology, rationalIntervals)45proof46  constructor47  . exact rationalIntervals.open48  . intros U hU x hx49    have parts := realTopology.membership.forward with hU50    have inside := powerset.membership_iff.forward with parts.left51    have realX := inside with x, hx52    obtain ⟨E, hE, positive, below⟩ := parts.right with x, hx53    have lowerReal : x - E ∈ ℝ by typecheck54    have upperReal : x + E ∈ ℝ by typecheck55    have lowerLess : x - E < x by linarith56    have upperLess : x < x + E by linarith57    obtain ⟨p, hp, lowerP, upperP⟩ := rationalCut.between with lowerLess58    obtain ⟨q, hq, lowerQ, upperQ⟩ := rationalCut.between with upperLess59    have realP := rationalCut.real at p with hp60    have realQ := rationalCut.real at q with hq61    have cutsOrdered := realLess.transitive with upperP, lowerQ62    have proper := realLess.characterization.forward with cutsOrdered63    have ordered := rationalCut.lt_of_cut_lt with proper64    have found := openInterval.member_intervals with ordered65    have center : x ∈ openInterval(rationalCut(p), rationalCut(q)) :=66      openInterval.membership.backward with ⟨realX, upperP, lowerQ⟩67    refine ⟨openInterval(rationalCut(p), rationalCut(q)), found, center, ?_⟩68    . intros y hy69      obtain ⟨realY, lowerY, upperY⟩ :=70        openInterval.membership.forward with hy71      have bounds : x - E < y ∧ y < x + E72        constructor73        . linarith74        . linarith75      have inBall := openBall.order_characterization.backward with bounds76      exact below with y, inBall7778-- The pairs of rationals in increasing order index the rational intervals.79def rationalPairs : Set :=80  { r ∈ ℚ × ℚ | relates(rationalLess, fst(r), snd(r)) }8182theorem rationalPairs.countable83  shows Countable(rationalPairs)84proof85  have rationals := rationals.countable86  have pairs := Countable.product at ℚ, ℚ with rationals, rationals87  have subset : rationalPairs ⊆ ℚ × ℚ88    intros r hr89    have parts := rationalPairs.membership.forward with hr90    exact parts.left91  exact Countable.subset with pairs, subset9293defgraph rationalInterval (r ∈ rationalPairs) : rationalIntervals :=94  openInterval(rationalCut(fst(r)), rationalCut(snd(r)))95proof96  have parts := rationalPairs.membership.forward with member97  obtain ⟨bound, p, hp, q, hq, shape⟩ :=98    product.membership.forward with parts.left99  have less := parts.right100  rw [shape, fst.pair, snd.pair] at less101  rw [shape, fst.pair, snd.pair]102  exact openInterval.member_intervals with less103104theorem rationalInterval.surjective105  shows SurjectiveBetween(rationalInterval, rationalPairs, rationalIntervals)106proof107  constructor108  . exact rationalInterval.function109  . intros W hW110    have parts := rationalIntervals.membership.forward with hW111    obtain ⟨p, hp, q, hq, less, shape⟩ := parts.right112    have pairIn : (p, q) ∈ ℚ × ℚ := product.pair with hp, hq113    have inPairs : (p, q) ∈ rationalPairs114      apply rationalPairs.membership.backward115      refine ⟨pairIn, ?_⟩116      rw [fst.pair, snd.pair]117      exact less118    have value := rationalInterval.relates with inPairs119    rw [fst.pair, snd.pair, ← shape] at value120    exact ⟨(p, q), inPairs, value⟩121122theorem rationalIntervals.countable123  shows Countable(rationalIntervals)124proof125  have countable := rationalPairs.countable126  have surjection := rationalInterval.surjective127  exact Countable.of_surjection with countable, surjection128