Grace/Cumulus/Topology/Continuity.g17

Open in Workbench Download source

Imports

Space

Declarations

Source

1-- Continuous maps between topological spaces: preimages of open sets are2-- open. Identity and composition, the closed-set characterisation, the3-- closure inclusion, and homeomorphisms4-- 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.Continuity10import Space1112predicate ContinuousMap (f X T Y S : Set) :=13  FunctionBetween(f, X, Y) ∧ (∀ V ∈ S, functionPreimage(f, X, V) ∈ T)1415predicate IsHomeomorphism (f X T Y S : Set) :=16  BijectiveBetween(f, X, Y) ∧ ContinuousMap(f, X, T, Y, S) ∧17  ContinuousMap(converse(f, X, Y), Y, S, X, T)1819theorem ContinuousMap.function (f X T Y S : Set)20  requires continuous : ContinuousMap(f, X, T, Y, S)21  shows f : X → Y22proof23  exact continuous.left2425theorem ContinuousMap.preimage (f X T Y S V : Set)26  requires continuous : ContinuousMap(f, X, T, Y, S)27  requires hV : V ∈ S28  shows functionPreimage(f, X, V) ∈ T29proof30  exact continuous.right with V, hV3132theorem ContinuousMap.identity (X T : Set)33  requires topology : IsTopology(X, T)34  shows ContinuousMap(identity(X), X, T, X, T)35proof36  have function := identity.function at X37  constructor38  . exact function39  . intros V hV40    have inside := IsTopology.subset with topology, hV41    have same : functionPreimage(identity(X), X, V) = V42      ext x43      constructor44      . intro hx45        have parts := functionPreimage.membership.forward with hx46        have fixed := identity.apply with parts.left47        rw fixed at parts48        exact parts.right49      . intro hx50        have hxX := inside with x, hx51        have fixed := identity.apply with hxX52        apply functionPreimage.membership.backward53        rw fixed54        exact ⟨hxX, hx⟩55    rwa same5657theorem ContinuousMap.compose (g f X T Y S Z R : Set)58  requires first : ContinuousMap(f, X, T, Y, S)59  requires second : ContinuousMap(g, Y, S, Z, R)60  shows ContinuousMap(compose(g, f, X, Y, Z), X, T, Z, R)61proof62  have fFunction := first.left63  have gFunction := second.left64  constructor65  . exact compose.function with fFunction, gFunction66  . intros W hW67    have step := functionPreimage.compose at g, f, X, Y, Z, W with fFunction, gFunction68    rw step69    have inner := second.right with W, hW70    exact first.right with functionPreimage(g, Y, W), inner7172theorem ContinuousMap.closed_preimage (f X T Y S C : Set)73  requires continuous : ContinuousMap(f, X, T, Y, S)74  requires closed : IsClosed(Y, S, C)75  shows IsClosed(X, T, functionPreimage(f, X, C))76proof77  have function := continuous.left78  constructor79  . exact functionPreimage.subset at f, X, C80  . have isOpen := continuous.right with complement(Y, C), closed.right81    have swap := functionPreimage.complement at f, X, Y, C with function82    unfold complement at isOpen83    rw swap at isOpen84    unfold complement85    exact isOpen8687theorem ContinuousMap.of_closed_preimages (f X T Y S : Set)88  requires topologyX : IsTopology(X, T)89  requires topologyY : IsTopology(Y, S)90  requires function : f : X → Y91  requires closed : ∀ C, IsClosed(Y, S, C) → IsClosed(X, T, functionPreimage(f, X, C))92  shows ContinuousMap(f, X, T, Y, S)93proof94  constructor95  . exact function96  . intros V hV97    have closedV := Open.complement_closed with topologyY, hV98    have closedPreimage := closed with complement(Y, V), closedV99    have swap := functionPreimage.complement at f, X, Y, V with function100    unfold complement at closedPreimage101    rw swap at closedPreimage102    have inside := functionPreimage.subset at f, X, V103    have double := complement.complement with inside104    have isOpen := closedPreimage.right105    have fold : complement(X, functionPreimage(f, X, V)) = X ∖ functionPreimage(f, X, V)106      unfold complement107      rfl108    rwa [← fold, double] at isOpen109110-- A continuous map sends the closure of A into the closure of its image.111theorem ContinuousMap.image_closure (f X T Y S A : Set)112  requires topologyX : IsTopology(X, T)113  requires topologyY : IsTopology(Y, S)114  requires continuous : ContinuousMap(f, X, T, Y, S)115  requires hA : A ⊆ X116  shows functionImage(f, closure(X, T, A), Y) ⊆ closure(Y, S, functionImage(f, A, Y))117proof118  have function := continuous.left119  have closureInside := closure.subset with topologyX, hA120  have imageInside := functionImage.subset at f, A, Y121  intros y hy122  simp [functionImage.membership] at hy123  obtain ⟨hyY, x, hx, shape⟩ := hy124  apply closure.membership.backward with topologyY, imageInside125  refine ⟨hyY, ?_⟩126  intros V hV hyV127  have hxX := closureInside with x, hx128  have preimageOpen := continuous.right with V, hV129  have hxPreimage : x ∈ functionPreimage(f, X, V)130    apply functionPreimage.membership.backward131    rw ← shape132    exact ⟨hxX, hyV⟩133  have touches := closure.membership.forward with topologyX, hA, hx134  obtain ⟨a, ha⟩ := touches.right with functionPreimage(f, X, V), preimageOpen, hxPreimage135  have parts := intersection.membership.forward with ha136  have preimageParts := functionPreimage.membership.forward with parts.left137  witness f(a)138  apply intersection.membership.backward139  constructor140  . exact preimageParts.right141  . have value := FunctionBetween.apply_closed with function, preimageParts.left142    simp [functionImage.membership]143    constructor144    . exact value145    . witness a146      constructor147      . exact parts.right148      . rfl149150theorem IsHomeomorphism.inverse (f X T Y S : Set)151  requires homeomorphism : IsHomeomorphism(f, X, T, Y, S)152  shows IsHomeomorphism(converse(f, X, Y), Y, S, X, T)153proof154  obtain ⟨bijective, forward, backward⟩ := homeomorphism155  have inverse := converse.bijective with bijective156  refine ⟨inverse, backward, ?_⟩157  have relation := FunctionBetween.relation with (Injective.function with (Bijective.injective with bijective))158  have same := converse.converse with relation159  rwa same160