Grace/Cumulus/Topology/Real.g17

Open in Workbench Download source

Imports

Subspace · Real.Analysis.OpenIntervals

Declarations

Source

1-- The standard topology on the real line: a set is open when every point2-- has an open ball inside it. Open balls and open intervals are open,3-- closed intervals are closed, the line is Hausdorff, and ε–δ continuity is topological4-- continuity5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Topology.Real11import Subspace12import Real.Analysis.OpenIntervals1314def realTopology : Set :=15  { U ∈ 𝒫(ℝ) | ∀ x ∈ U, ∃ E ∈ ℝ, 0 < E ∧ openBall(x, E) ⊆ U }1617theorem openBall.subset_reals (C E : Real)18  shows openBall(C, E) ⊆ ℝ19proof20  intros x hx21  have parts := openBall.membership.forward with hx22  exact parts.left2324theorem openBall.open (C E : Real)25  shows openBall(C, E) ∈ realTopology26proof27  apply realTopology.membership.backward28  refine ⟨(powerset.membership_iff.backward with (openBall.subset_reals at C, E)), ?_⟩29  intros x hx30  obtain ⟨realX, near⟩ := openBall.membership.forward with hx31  have radiusReal : E - dist(x, C) ∈ ℝ by typecheck32  have positive : (0:R) < E - dist(x, C) by linarith33  refine ⟨E - dist(x, C), radiusReal, positive, ?_⟩34  intros y hy35  obtain ⟨realY, nearY⟩ := openBall.membership.forward with hy36  apply openBall.membership.backward37  refine ⟨realY, ?_⟩38  have triangle := dist.triangle at y, x, C39  linarith4041theorem realTopology.topology42  shows IsTopology(ℝ, realTopology)43proof44  constructor45  . intros U hU46    have parts := realTopology.membership.forward with hU47    exact parts.left48  . constructor49    . apply realTopology.membership.backward50      refine ⟨(powerset.self at ℝ), ?_⟩51      intros x hx52      have one : (1:R) ∈ ℝ by typecheck53      have positive : (0:R) < 1 by linarith54      refine ⟨(1:R), one, positive, (openBall.subset_reals at x, (1:R))⟩55    . constructor56      . intros S hS57        apply realTopology.membership.backward58        constructor59        . apply powerset.membership_iff.backward60          apply union.subset61          intros U hU62          have parts := realTopology.membership.forward with (hS with U, hU)63          exact powerset.membership_iff.forward with parts.left64        . intros x hx65          obtain ⟨U, hU, hxU⟩ := union.membership.forward with hx66          have parts := realTopology.membership.forward with (hS with U, hU)67          obtain ⟨E, hE, positive, inside⟩ := parts.right with x, hxU68          refine ⟨E, hE, positive, ?_⟩69          exact Subset.transitive with inside, (union.subset_of_member with hU)70      . intros U hU V hV71        have partsU := realTopology.membership.forward with hU72        have partsV := realTopology.membership.forward with hV73        have insideU := powerset.membership_iff.forward with partsU.left74        apply realTopology.membership.backward75        constructor76        . apply powerset.membership_iff.backward77          exact Subset.transitive with (intersection.subset_left at U, V), insideU78        . intros x hx79          have both := intersection.membership.forward with hx80          have realX := insideU with x, both.left81          obtain ⟨E1, hE1, positive1, inside1⟩ := partsU.right with x, both.left82          obtain ⟨E2, hE2, positive2, inside2⟩ := partsV.right with x, both.right83          have order := realLess.trichotomy at E1, E284          cases order with smaller | rest85          . have le := realLess.implies_le with smaller86            refine ⟨E1, hE1, positive1, ?_⟩87            apply intersection.greatest88            . exact inside189            . have ballMono : openBall(x, E1) ⊆ openBall(x, E2)90                intros w hw91                have ballInside := openBall.subset_reals at x, E192                have realY := ballInside with w, hw93                exact openBall.mono with hw, le94              exact Subset.transitive with ballMono, inside295          . cases rest with equal | larger96            . refine ⟨E1, hE1, positive1, ?_⟩97              apply intersection.greatest98              . exact inside199              . rw equal100                exact inside2101            . have le := realLess.implies_le with larger102              refine ⟨E2, hE2, positive2, ?_⟩103              apply intersection.greatest104              . have ballMono : openBall(x, E2) ⊆ openBall(x, E1)105                  intros w hw106                  have ballInside := openBall.subset_reals at x, E2107                  have realY := ballInside with w, hw108                  exact openBall.mono with hw, le109                exact Subset.transitive with ballMono, inside1110              . exact inside2111112theorem realTopology.hausdorff113  shows IsHausdorff(ℝ, realTopology)114proof115  intros x hx y hy distinct116  have positive := dist.positive_of_ne with distinct117  have halfPositive := half.positive with positive118  refine ⟨openBall(x, half(dist(x, y))), (openBall.open at x, half(dist(x, y))), openBall(y, half(dist(x, y))), (openBall.open at y, half(dist(x, y))), (openBall.center with halfPositive), ?_, ?_⟩119  . exact openBall.center with halfPositive120  . apply Disjoint.iff.backward121    intros z hz hz2122    have ballInside := openBall.subset_reals at x, half(dist(x, y))123    have realZ := ballInside with z, hz124    have same := openBall.half_radius_unique with hz, hz2125    exact distinct with same126127-- Closed intervals are closed: a point outside has a ball that stays128-- outside.129theorem closedInterval.closed (A B : Real)130  shows IsClosed(ℝ, realTopology, closedInterval(A, B))131proof132  constructor133  . exact closedInterval.subset_reals at A, B134  . apply realTopology.membership.backward135    constructor136    . exact powerset.membership_iff.backward with (complement.subset at ℝ, closedInterval(A, B))137    . intros x hx138      have parts := complement.membership.forward with hx139      have realX := parts.left140      have outside : x < A ∨ B < x141        have orderA := realLess.trichotomy at x, A142        cases orderA with belowA | restA143        . left144          exact belowA145        . right146          have aboveA : A ≤ x147            cases restA with equalA | aboveA148            . rw equalA149              exact realLe.reflexive150            . exact realLess.implies_le with aboveA151          have orderB := realLess.trichotomy at x, B152          cases orderB with belowB | restB153          . exfalso154            apply parts.right155            apply closedInterval.membership.backward156            exact ⟨realX, aboveA, (realLess.implies_le with belowB)⟩157          . cases restB with equalB | aboveB158            . exfalso159              apply parts.right160              apply closedInterval.membership.backward161              have le : x ≤ B162                rw equalB163                exact realLe.reflexive164              exact ⟨realX, aboveA, le⟩165            . exact aboveB166      cases outside with belowA | aboveB167      . have radiusReal : A - x ∈ ℝ by typecheck168        have positive : (0:R) < A - x by linarith169        refine ⟨A - x, radiusReal, positive, ?_⟩170        intros y hy171        obtain ⟨realY, near⟩ := openBall.membership.forward with hy172        unfold dist at near173        have upper := abs.upper at y - x174        apply complement.membership.backward175        refine ⟨realY, ?_⟩176        intro member177        obtain ⟨realY2, lower, upperY⟩ := closedInterval.membership.forward with member178        linarith179      . have radiusReal : x - B ∈ ℝ by typecheck180        have positive : (0:R) < x - B by linarith181        refine ⟨x - B, radiusReal, positive, ?_⟩182        intros y hy183        obtain ⟨realY, near⟩ := openBall.membership.forward with hy184        unfold dist at near185        have upper := abs.upper_neg at y - x186        apply complement.membership.backward187        refine ⟨realY, ?_⟩188        intro member189        obtain ⟨realY2, lower, upperY⟩ := closedInterval.membership.forward with member190        linarith191192-- Open intervals are open.193theorem openInterval.open (A B : Real)194  shows openInterval(A, B) ∈ realTopology195proof196  apply realTopology.membership.backward197  have inside := openInterval.subset_reals at A, B198  refine ⟨(powerset.membership_iff.backward with inside), ?_⟩199  intros x hx200  obtain ⟨realX, lower, upper⟩ := openInterval.membership.forward with hx201  have leftReal : x - A ∈ ℝ by typecheck202  have rightReal : B - x ∈ ℝ by typecheck203  have split : x - A ≤ B - x ∨ ¬(x - A ≤ B - x) by tauto204  cases split with leftSmaller | rightSmaller205  . have positive : (0:R) < x - A by linarith206    refine ⟨x - A, leftReal, positive, ?_⟩207    apply openInterval.ball_subset208    . linarith209    . linarith210  . have order := realLess.of_not_le with rightSmaller211    have positive : (0:R) < B - x by linarith212    refine ⟨B - x, rightReal, positive, ?_⟩213    apply openInterval.ball_subset214    . linarith215    . linarith216217-- ε–δ continuity on the line is continuity for the standard topology.218theorem Continuous.continuous_map (f : Set)219  shows Continuous(f) ↔ ContinuousMap(f, ℝ, realTopology, ℝ, realTopology)220proof221  constructor222  . intro continuous223    obtain ⟨function, pointwise⟩ := continuous224    constructor225    . exact function226    . intros V hV227      have partsV := realTopology.membership.forward with hV228      apply realTopology.membership.backward229      constructor230      . exact powerset.membership_iff.backward with (functionPreimage.subset at f, ℝ, V)231      . intros x hx232        have inPreimage := functionPreimage.membership.forward with hx233        obtain ⟨E, hE, positive, ballInside⟩ := partsV.right with f(x), inPreimage.right234        obtain ⟨function2, control⟩ := pointwise with x, inPreimage.left235        obtain ⟨D, hD, positiveD, maps⟩ := control with E, hE, positive236        refine ⟨D, hD, positiveD, ?_⟩237        intros y hy238        have ballInsideD := openBall.subset_reals at x, D239        have realY := ballInsideD with y, hy240        apply functionPreimage.membership.backward241        refine ⟨realY, ?_⟩242        exact ballInside with f(y), (maps with y, realY, hy)243  . intro continuousMap244    obtain ⟨function, preimages⟩ := continuousMap245    constructor246    . exact function247    . intros a ha248      constructor249      . exact function250      . intros E hE positive251        have ballOpen := openBall.open at f(a), E252        have preimageOpen := preimages with openBall(f(a), E), ballOpen253        have parts := realTopology.membership.forward with preimageOpen254        have center := openBall.center at f(a), E with positive255        have inPreimage : a ∈ functionPreimage(f, ℝ, openBall(f(a), E)) := functionPreimage.membership.backward with ⟨ha, center⟩256        obtain ⟨D, hD, positiveD, inside⟩ := parts.right with a, inPreimage257        refine ⟨D, hD, positiveD, ?_⟩258        intros x hx near259        have member := inside with x, near260        have parts2 := functionPreimage.membership.forward with member261        exact parts2.right262