Grace/Cumulus/Topology/Continuous.g17

Open in Workbench Download source

Imports

Structure

Declarations

Source

1-- Continuous maps between bundled spaces: the guard f : X ⇒ Y, the2-- identity, composition, constants, and restrictions, preimages of open and3-- closed sets, the closure inclusion, convergent sequences under a4-- continuous map, compact images, and homeomorphisms5-- 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.Continuous11import Structure1213-- f : X ⇒ Y: a function between the carriers of two spaces under which the14-- preimage of every open set is open. The form is a transparent guard, so15-- a hypothesis f : X ⇒ Y also supplies the spaces X and Y and the binders16-- (x : X) and (y : Y). ContinuousMap(f, A, T, B, S) remains the form over17-- separate pieces, bridged below.18predicate Continuous (f X Y : Set) :=19  TopologicalSpace(X) ∧ TopologicalSpace(Y) ∧20  ContinuousMap(f, X.carrier, X.opens, Y.carrier, Y.opens)2122notation guard "_ : _ ⇒ _" => Continuous2324theorem Continuous.mk (f X Y : Set)25  requires source : TopologicalSpace(X)26  requires target : TopologicalSpace(Y)27  requires function : f : X.carrier → Y.carrier28  requires preimages :29    ∀ V ∈ Y.opens, functionPreimage(f, X.carrier, V) ∈ X.opens30  shows f : X ⇒ Y31proof32  unfold Continuous33  refine ⟨source, target, ?_⟩34  unfold ContinuousMap35  exact ⟨function, preimages⟩3637theorem Continuous.of_projections (f X Y : Set)38  requires spaceX : TopologicalSpace(X)39  requires spaceY : TopologicalSpace(Y)40  requires continuous : ContinuousMap(f, X.carrier, X.opens, Y.carrier, Y.opens)41  shows f : X ⇒ Y42proof43  unfold Continuous44  exact ⟨spaceX, spaceY, continuous⟩4546theorem Continuous.of_parts (f A T B S : Set)47  requires topologyA : IsTopology(A, T)48  requires topologyB : IsTopology(B, S)49  requires continuous : ContinuousMap(f, A, T, B, S)50  shows f : TopologicalSpace.mk(A, T) ⇒ TopologicalSpace.mk(B, S)51proof52  have spaceA := TopologicalSpace.of_parts with topologyA53  have spaceB := TopologicalSpace.of_parts with topologyB54  unfold Continuous55  refine ⟨spaceA, spaceB, ?_⟩56  topology_projections5758section ContinuityLaws59variable (f X Y : Set)60hypothesis continuous : f : X ⇒ Y6162theorem Continuous.source63  shows TopologicalSpace(X)64proof65  obtain ⟨source, rest⟩ := continuous66  exact source6768theorem Continuous.target69  shows TopologicalSpace(Y)70proof71  obtain ⟨source, target, rest⟩ := continuous72  exact target7374-- The bridge to the form over separate pieces is an instance, so `with *`75-- reads it off the guard.76instance Continuous.parts77  shows ContinuousMap(f, X.carrier, X.opens, Y.carrier, Y.opens)78proof79  obtain ⟨source, target, engine⟩ := continuous80  exact engine8182theorem Continuous.function_between83  shows f : X.carrier → Y.carrier84proof85  have engine := Continuous.parts with continuous86  exact ContinuousMap.function with engine8788theorem Continuous.apply_mem (x : X)89  shows f(x) ∈ Y90proof91  have function := Continuous.function_between with continuous92  have xIn : x ∈ X by assumption93  exact FunctionBetween.apply_closed with function, xIn9495theorem Continuous.preimage_open (V : Set)96  requires open : Open(Y, V)97  shows Open(X, functionPreimage(f, X.carrier, V))98proof99  have spaceX := Continuous.source with continuous100  have engine := Continuous.parts with continuous101  have member := Open.mem with open102  exact Open.of_mem with spaceX, (ContinuousMap.preimage with engine, member)103104theorem Continuous.preimage_closed (C : Set)105  requires closed : Closed(Y, C)106  shows Closed(X, functionPreimage(f, X.carrier, C))107proof108  have spaceX := Continuous.source with continuous109  have engine := Continuous.parts with continuous110  have pieces := Closed.parts with closed111  have closedPreimage := ContinuousMap.closed_preimage with engine, pieces112  exact Closed.of_parts with spaceX, closedPreimage113114-- A continuous map sends the closure of A into the closure of its image.115theorem Continuous.image_closure (A : Set)116  requires hA : A ⊆ X117  shows functionImage(f, closure(X, A), Y.carrier) ⊆118    closure(Y, functionImage(f, A, Y.carrier))119proof120  have engine := Continuous.parts with continuous121  rw [closure.parts, closure.parts]122  exact ContinuousMap.image_closure with *123124-- A continuous map carries a convergent sequence to a convergent sequence.125theorem Continuous.map_converges (u : Set) (x : X)126  requires converges : u ⇝ x127  shows compose(f, u, ℕ, X.carrier, Y.carrier) ⇝ f(x)128proof129  have function := Continuous.function_between with continuous130  have sequence := Converges.sequence with converges131  have point := Converges.limit_mem with converges132  have composite := compose.function with sequence, function133  have image := FunctionBetween.apply_closed with function, point134  have eventually : ∀ V, Open(Y, V) → f(x) ∈ V →135      ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →136        apply(compose(f, u, ℕ, X.carrier, Y.carrier), n) ∈ V137    intros V open hfx138    have preimageOpen := Continuous.preimage_open with continuous, open139    have inPreimage : x ∈ functionPreimage(f, X.carrier, V)140      apply functionPreimage.membership.backward141      exact ⟨point, hfx⟩142    have hit := Converges.eventually with converges, preimageOpen, inPreimage143    obtain ⟨N, hN, tail⟩ := hit144    witness N145    refine ⟨hN, ?_⟩146    intros n hn order147    have term := tail with n, hn, order148    have parts := functionPreimage.membership.forward with term149    have value := compose.apply at f, u, ℕ, X.carrier, Y.carrier, n with *150    rw value151    exact parts.right152  exact Converges.of_eventually with *153154-- The continuous image of a compact set is compact.155theorem Compact.continuous_image (A : Set)156  requires compact : Compact(X, A)157  shows Compact(Y, functionImage(f, A, Y.carrier))158proof159  have engine := Continuous.parts with continuous160  have pieces := Compact.parts with compact161  exact Compact.of_parts with (IsCompact.image with engine, pieces)162163end ContinuityLaws164165theorem Continuous.id (X : Set)166  requires space : TopologicalSpace(X)167  shows identity(X.carrier) : X ⇒ X168proof169  unfold Continuous170  refine ⟨space, space, ?_⟩171  exact ContinuousMap.identity with *172173theorem Continuous.comp (f g X Y Z : Set)174  requires first : f : X ⇒ Y175  requires second : g : Y ⇒ Z176  shows compose(g, f, X.carrier, Y.carrier, Z.carrier) : X ⇒ Z177proof178  have engineF := Continuous.parts with first179  have engineG := Continuous.parts with second180  unfold Continuous181  have spaceX := Continuous.source with first182  have spaceZ := Continuous.target with second183  refine ⟨spaceX, spaceZ, ?_⟩184  exact ContinuousMap.compose with engineF, engineG185186theorem Continuous.constant (X Y y : Set)187  requires spaceX : TopologicalSpace(X)188  requires spaceY : TopologicalSpace(Y)189  requires hy : y ∈ Y190  shows constantFunction(X.carrier, Y.carrier, y) : X ⇒ Y191proof192  unfold Continuous193  refine ⟨spaceX, spaceY, ?_⟩194  exact ContinuousMap.constant with *195196theorem Continuous.of_closed_preimages (f X Y : Set)197  requires spaceX : TopologicalSpace(X)198  requires spaceY : TopologicalSpace(Y)199  requires function : f : X.carrier → Y.carrier200  requires closed :201    ∀ C, Closed(Y, C) → Closed(X, functionPreimage(f, X.carrier, C))202  shows f : X ⇒ Y203proof204  have pieces : ∀ C, IsClosed(Y.carrier, Y.opens, C) →205      IsClosed(X.carrier, X.opens, functionPreimage(f, X.carrier, C))206    intros C closedC207    exact Closed.parts with (closed with C, (Closed.of_parts with closedC))208  unfold Continuous209  refine ⟨spaceX, spaceY, ?_⟩210  exact ContinuousMap.of_closed_preimages with *211212-- Homeomorphisms: continuous bijections with a continuous inverse.213predicate Homeomorphism (f X Y : Set) :=214  Continuous(f, X, Y) ∧ BijectiveBetween(f, X.carrier, Y.carrier) ∧215  Continuous(converse(f, X.carrier, Y.carrier), Y, X)216217theorem Homeomorphism.continuous (f X Y : Set)218  requires homeomorphism : Homeomorphism(f, X, Y)219  shows f : X ⇒ Y220proof221  obtain ⟨continuous, rest⟩ := homeomorphism222  exact continuous223224theorem Homeomorphism.bijective (f X Y : Set)225  requires homeomorphism : Homeomorphism(f, X, Y)226  shows BijectiveBetween(f, X.carrier, Y.carrier)227proof228  obtain ⟨continuous, bijective, inverse⟩ := homeomorphism229  exact bijective230231instance Homeomorphism.parts (f X Y : Set)232  requires homeomorphism : Homeomorphism(f, X, Y)233  shows IsHomeomorphism(f, X.carrier, X.opens, Y.carrier, Y.opens)234proof235  obtain ⟨continuous, bijective, inverse⟩ := homeomorphism236  have forward := Continuous.parts with continuous237  have backward := Continuous.parts with inverse238  unfold IsHomeomorphism239  exact ⟨bijective, forward, backward⟩240241theorem Homeomorphism.of_parts (f X Y : Set)242  requires spaceX : TopologicalSpace(X)243  requires spaceY : TopologicalSpace(Y)244  requires homeomorphism :245    IsHomeomorphism(f, X.carrier, X.opens, Y.carrier, Y.opens)246  shows Homeomorphism(f, X, Y)247proof248  obtain ⟨bijective, forward, backward⟩ := homeomorphism249  have continuous : f : X ⇒ Y250    unfold Continuous251    exact ⟨spaceX, spaceY, forward⟩252  have inverse : converse(f, X.carrier, Y.carrier) : Y ⇒ X253    unfold Continuous254    exact ⟨spaceY, spaceX, backward⟩255  unfold Homeomorphism256  exact ⟨continuous, bijective, inverse⟩257258theorem Homeomorphism.symm (f X Y : Set)259  requires homeomorphism : Homeomorphism(f, X, Y)260  shows Homeomorphism(converse(f, X.carrier, Y.carrier), Y, X)261proof262  have continuous := Homeomorphism.continuous with homeomorphism263  have spaceX := Continuous.source with continuous264  have spaceY := Continuous.target with continuous265  have engine := Homeomorphism.parts with homeomorphism266  apply Homeomorphism.of_parts with spaceY, spaceX267  exact Continuity.IsHomeomorphism.inverse with engine268