Grace/Cumulus/Topology/Spaces.g17

Open in Workbench Download source

Imports

Continuous · Plane

Declarations

Source

1-- Spaces built from spaces and the properties of a space: subspaces,2-- products, the real line and the plane as values; compactness, the3-- Hausdorff and T1 properties, connectedness, and their laws, with the4-- tube lemma, Heine–Borel, compact subsets of Hausdorff spaces, and the5-- uniqueness of limits in their textbook statements6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Topology.Spaces12import Continuous13import Plane1415-- The subspace on a subset, the product of two spaces, the real line, and16-- the plane, each a constructed space whose projections are the carrier17-- and topology over separate pieces.18def subspace (X A : Set) : Set :=19  TopologicalSpace.mk(A, subspaceTopology(TopologicalSpace.opens(X), A))20def productSpace (X Y : Set) : Set :=21  TopologicalSpace.mk(22    TopologicalSpace.carrier(X) × TopologicalSpace.carrier(Y),23    productTopology(TopologicalSpace.carrier(X), TopologicalSpace.opens(X),24      TopologicalSpace.carrier(Y), TopologicalSpace.opens(Y)))25def realLine : Set := TopologicalSpace.mk(ℝ, realTopology)26def plane : Set := TopologicalSpace.mk(ℝ × ℝ, planeTopology)2728theorem subspace.carrier (X A : Set)29  shows TopologicalSpace.carrier(subspace(X, A)) = A30proof31  unfold subspace32  topology_projections3334theorem subspace.opens (X A : Set)35  shows TopologicalSpace.opens(subspace(X, A)) =36    subspaceTopology(TopologicalSpace.opens(X), A)37proof38  unfold subspace39  topology_projections4041theorem productSpace.carrier (X Y : Set)42  shows TopologicalSpace.carrier(productSpace(X, Y)) =43    TopologicalSpace.carrier(X) × TopologicalSpace.carrier(Y)44proof45  unfold productSpace46  topology_projections4748theorem productSpace.opens (X Y : Set)49  shows TopologicalSpace.opens(productSpace(X, Y)) =50    productTopology(TopologicalSpace.carrier(X), TopologicalSpace.opens(X),51      TopologicalSpace.carrier(Y), TopologicalSpace.opens(Y))52proof53  unfold productSpace54  topology_projections5556theorem realLine.carrier57  shows TopologicalSpace.carrier(realLine) = ℝ58proof59  unfold realLine60  topology_projections6162theorem realLine.opens63  shows TopologicalSpace.opens(realLine) = realTopology64proof65  unfold realLine66  topology_projections6768theorem plane.carrier69  shows TopologicalSpace.carrier(plane) = ℝ × ℝ70proof71  unfold plane72  topology_projections7374theorem plane.opens75  shows TopologicalSpace.opens(plane) = planeTopology76proof77  unfold plane78  topology_projections7980-- Each construction is a space; these are instances, so the hypothesis on81-- a constructed space is synthesized from those on its pieces.82instance subspace.space (X A : Set)83  requires space : TopologicalSpace(X)84  requires hA : A ⊆ X85  shows TopologicalSpace(subspace(X, A))86proof87  have parts := TopologicalSpace.parts with space88  have topology := subspaceTopology.topology with parts, hA89  unfold subspace90  exact TopologicalSpace.of_parts with topology9192instance productSpace.space (X Y : Set)93  requires spaceX : TopologicalSpace(X)94  requires spaceY : TopologicalSpace(Y)95  shows TopologicalSpace(productSpace(X, Y))96proof97  have partsX := TopologicalSpace.parts with spaceX98  have partsY := TopologicalSpace.parts with spaceY99  have topology := productTopology.topology with partsX, partsY100  unfold productSpace101  exact TopologicalSpace.of_parts with topology102103instance realLine.space104  shows TopologicalSpace(realLine)105proof106  unfold realLine107  exact TopologicalSpace.of_parts with realTopology.topology108109instance plane.space110  shows TopologicalSpace(plane)111proof112  unfold plane113  exact TopologicalSpace.of_parts with planeTopology.topology114115theorem plane.eq_product116  shows plane = productSpace(realLine, realLine)117proof118  unfold plane119  unfold productSpace120  unfold planeTopology121  rw [realLine.carrier, realLine.opens]122  rfl123124section CompactLaws125variable (X : Set)126hypothesis space : TopologicalSpace(X)127128theorem Compact.subset_carrier (A : Set)129  requires compact : Compact(X, A)130  shows A ⊆ X131proof132  have pieces := Compact.parts with compact133  exact Compact.IsCompact.subset with pieces134135instance Compact.empty_set136  shows Compact(X, ∅)137proof138  exact Compact.of_parts with (Compact.IsCompact.empty at X.carrier, X.opens)139140instance Compact.point (x : X)141  shows Compact(X, {x})142proof143  have xIn : x ∈ X by assumption144  have point := Compact.IsCompact.singleton at X.carrier, X.opens, x with xIn145  exact Compact.of_parts with point146147instance Compact.union (A B : Set)148  requires compactA : Compact(X, A)149  requires compactB : Compact(X, B)150  shows Compact(X, A ∪ B)151proof152  have piecesA := Compact.parts with compactA153  have piecesB := Compact.parts with compactB154  exact Compact.of_parts with (Compact.IsCompact.union2 with piecesA, piecesB)155156theorem Compact.of_finite (A : Set)157  requires finite : Finite(A)158  requires hA : A ⊆ X159  shows Compact(X, A)160proof161  have engine := CompactMore.IsCompact.finite at X.carrier, X.opens, A with *162  exact Compact.of_parts with engine163164-- A closed subset of a compact set is compact.165theorem Compact.of_closed_subset (A C : Set)166  requires compact : Compact(X, A)167  requires closed : Closed(X, C)168  requires hCA : C ⊆ A169  shows Compact(X, C)170proof171  have parts := TopologicalSpace.parts with space172  have piecesA := Compact.parts with compact173  have piecesC := Closed.parts with closed174  have engine := Compact.IsCompact.closed_subset with parts, piecesA, piecesC,175    hCA176  exact Compact.of_parts with engine177178theorem Compact.space_iff179  shows Compact(X) ↔ Compact(X, X.carrier)180proof181  constructor182  . intro compact183    exact Compact.of_parts with (Compact.space_parts with compact)184  . intro compact185    exact Compact.of_space_parts with (Compact.parts with compact)186187theorem Compact.space_of_finite188  requires finite : Finite(X.carrier)189  shows Compact(X)190proof191  apply Compact.of_space_parts192  exact IsCompact.whole_of_finite at X.carrier, X.opens with finite193194end CompactLaws195196section HausdorffLaws197variable (X : Set)198hypothesis space : TopologicalSpace(X)199hypothesis hausdorff : Hausdorff(X)200201-- Distinct points have disjoint open neighborhoods.202theorem Hausdorff.separate (x y : X)203  requires distinct : x ≠ y204  shows ∃ U ∈ X.opens, ∃ V ∈ X.opens,205    x ∈ U ∧ y ∈ V ∧ Disjoint(U, V)206proof207  have parts := Hausdorff.parts with hausdorff208  have xIn : x ∈ X by assumption209  have yIn : y ∈ X by assumption210  exact parts with x, xIn, y, yIn, distinct211212instance Hausdorff.point_closed (x : X)213  shows Closed(X, {x})214proof215  have parts := TopologicalSpace.parts with space216  have pieces := Hausdorff.parts with hausdorff217  have xIn : x ∈ X by assumption218  have engine := Subspace.IsHausdorff.singleton_closed with parts, pieces, xIn219  exact Closed.of_parts with engine220221theorem Hausdorff.t1_space222  shows T1Space(X)223proof224  have pieces := Hausdorff.parts with hausdorff225  apply T1Space.of_parts226  exact Separation.IsHausdorff.t1 with pieces227228-- A compact subset of a Hausdorff space is closed.229theorem Compact.closed_of_hausdorff (K : Set)230  requires compact : Compact(X, K)231  shows Closed(X, K)232proof233  have parts := TopologicalSpace.parts with space234  have pieces := Hausdorff.parts with hausdorff235  have compactK := Compact.parts with compact236  have engine := IsCompact.hausdorff_closed with parts, pieces, compactK237  exact Closed.of_parts with engine238239-- In a compact Hausdorff space the compact subsets are the closed ones.240theorem Compact.iff_closed (K : Set)241  requires compact : Compact(X)242  shows Compact(X, K) ↔ Closed(X, K)243proof244  constructor245  . intro compactK246    exact Compact.closed_of_hausdorff with *247  . intro closed248    have whole := Compact.of_parts with (Compact.space_parts with compact)249    have inside := Closed.subset with closed250    exact Compact.of_closed_subset with whole, closed, inside251252-- A sequence has at most one limit.253theorem Converges.unique (u : Set) (x y : X)254  requires first : u ⇝ x255  requires second : u ⇝ y256  shows x = y257proof258  by_contra distinct259  obtain ⟨U, hU, V, hV, hxU, hyV, disjoint⟩ := Hausdorff.separate with *260  have separated := Disjoint.iff.forward with disjoint261  have openU := Open.of_mem with hU262  have openV := Open.of_mem with hV263  obtain ⟨N, hN, tailU⟩ := Converges.eventually with first, openU, hxU264  obtain ⟨M, hM, tailV⟩ := Converges.eventually with second, openV, hyV265  have order := LessEqual.total at N, M266  cases order with below | above267  . have inU := tailU with M, hM, below268    have inV := tailV with M, hM, (LessEqual.reflexive at M)269    exact separated with u(M), inU, inV270  . have inU := tailU with N, hN, (LessEqual.reflexive at N)271    have inV := tailV with N, hN, above272    exact separated with u(N), inU, inV273274end HausdorffLaws275276section ConnectedLaws277variable (X : Set)278hypothesis space : TopologicalSpace(X)279280theorem Connected.clopen_trivial (U : Set)281  requires connected : Connected(X)282  requires open : Open(X, U)283  requires closed : Closed(X, U)284  shows U = ∅ ∨ U = X.carrier285proof286  have parts := TopologicalSpace.parts with space287  have pieces := Connected.parts with connected288  have member := Open.mem with open289  have closedU := Closed.parts with closed290  exact Connected.IsConnected.clopen with parts, pieces, member, closedU291292theorem Connected.iff_clopen_trivial293  shows Connected(X) ↔294    ∀ U, Open(X, U) → Closed(X, U) → U = ∅ ∨ U = X.carrier295proof296  have parts := TopologicalSpace.parts with space297  have characterization := Connected.IsConnected.iff_clopen with parts298  constructor299  . intros connected U open closed300    exact Connected.clopen_trivial with *301  . intro trivial302    have pieces : ∀ U ∈ X.opens, IsClosed(X.carrier, X.opens, U) →303        U = ∅ ∨ U = X.carrier304      intros U hU closedU305      have openU := Open.of_mem with hU306      have closedB := Closed.of_parts with closedU307      exact trivial with U, openU, closedB308    exact Connected.of_parts with (characterization.backward with pieces)309310theorem ConnectedSubset.subset_carrier (A : Set)311  requires connected : ConnectedSubset(X, A)312  shows A ⊆ X313proof314  have pieces := ConnectedSubset.parts with connected315  exact Connected.IsConnectedSubset.subset with pieces316317-- A subset is connected exactly when it is connected as a subspace.318theorem ConnectedSubset.iff_subspace_connected (A : Set)319  requires hA : A ⊆ X320  shows ConnectedSubset(X, A) ↔ Connected(subspace(X, A))321proof322  have parts := TopologicalSpace.parts with space323  have characterization := Connected.IsConnectedSubset.iff_subspace with parts,324    hA325  constructor326  . intro connected327    have pieces := ConnectedSubset.parts with connected328    unfold subspace329    exact Connected.of_mk with (characterization.forward with pieces)330  . intro connected331    have pieces := Connected.parts with connected332    rw [subspace.carrier, subspace.opens] at pieces333    exact ConnectedSubset.of_parts with (characterization.backward with pieces)334335end ConnectedLaws336337-- The continuous image of a connected space is connected.338theorem Connected.continuous_image (f X Y : Set)339  requires continuous : f : X ⇒ Y340  requires connected : Connected(X)341  shows ConnectedSubset(Y, functionImage(f, X.carrier, Y.carrier))342proof343  have parts := TopologicalSpace.parts with (Continuous.source with continuous)344  have engine := Continuous.parts with continuous345  have pieces := Connected.parts with connected346  have target := Continuous.target with continuous347  have image := Connected.IsConnected.image with parts, engine, pieces348  exact ConnectedSubset.of_parts with target, image349350theorem ConnectedSubset.continuous_image (f X Y A : Set)351  requires continuous : f : X ⇒ Y352  requires connected : ConnectedSubset(X, A)353  shows ConnectedSubset(Y, functionImage(f, A, Y.carrier))354proof355  have engine := Continuous.parts with continuous356  have pieces := ConnectedSubset.parts with connected357  have target := Continuous.target with continuous358  have image := Connected.IsConnectedSubset.image with engine, pieces359  exact ConnectedSubset.of_parts with target, image360361-- Subspaces: the inclusion and restrictions are continuous, and the362-- Hausdorff and T1 properties pass to subspaces.363theorem Continuous.inclusion (X A : Set)364  requires space : TopologicalSpace(X)365  requires hA : A ⊆ X366  shows inclusionMap(A, X.carrier) : subspace(X, A) ⇒ X367proof368  have parts := TopologicalSpace.parts with space369  have engine := ContinuousMap.inclusion with parts, hA370  have spaceA : TopologicalSpace(subspace(X, A)) := subspace.space with *371  have shifted : ContinuousMap(inclusionMap(A, X.carrier),372      TopologicalSpace.carrier(subspace(X, A)),373      TopologicalSpace.opens(subspace(X, A)), X.carrier, X.opens)374    rw [subspace.carrier, subspace.opens]375    exact engine376  exact Continuous.of_projections with spaceA, space, shifted377378theorem Continuous.restrict (f X Y A : Set)379  requires continuous : f : X ⇒ Y380  requires hA : A ⊆ X381  shows restrict(f, A) : subspace(X, A) ⇒ Y382proof383  have spaceX := Continuous.source with continuous384  have spaceY := Continuous.target with continuous385  have engine := Continuous.parts with continuous386  have restricted := ContinuousMap.restrict with engine, hA387  have spaceA : TopologicalSpace(subspace(X, A)) := subspace.space with *388  have shifted : ContinuousMap(restrict(f, A),389      TopologicalSpace.carrier(subspace(X, A)),390      TopologicalSpace.opens(subspace(X, A)), Y.carrier, Y.opens)391    rw [subspace.carrier, subspace.opens]392    exact restricted393  exact Continuous.of_projections with spaceA, spaceY, shifted394395instance Hausdorff.subspace_of (X A : Set)396  requires space : TopologicalSpace(X)397  requires hausdorff : Hausdorff(X)398  requires hA : A ⊆ X399  shows Hausdorff(subspace(X, A))400proof401  have pieces := Hausdorff.parts with hausdorff402  unfold subspace403  exact Hausdorff.of_mk with (Separation.IsHausdorff.subspace with pieces, hA)404405theorem T1Space.subspace_of (X A : Set)406  requires space : TopologicalSpace(X)407  requires t1 : T1Space(X)408  requires hA : A ⊆ X409  shows T1Space(subspace(X, A))410proof411  have pieces := T1Space.parts with t1412  unfold subspace413  exact T1Space.of_mk with (Separation.IsT1Space.subspace with pieces, hA)414415-- Products: boxes are open, the projections are continuous, the product416-- of Hausdorff spaces is Hausdorff, and the product of compact sets is417-- compact (the tube lemma).418theorem Open.box (X Y U V : Set)419  requires spaceX : TopologicalSpace(X)420  requires spaceY : TopologicalSpace(Y)421  requires openU : Open(X, U)422  requires openV : Open(Y, V)423  shows Open(productSpace(X, Y), U × V)424proof425  have partsX := TopologicalSpace.parts with spaceX426  have partsY := TopologicalSpace.parts with spaceY427  have memberU := Open.mem with openU428  have memberV := Open.mem with openV429  have box := productTopology.box with partsX, partsY, memberU, memberV430  unfold productSpace431  exact Open.of_mk with (productTopology.topology with partsX, partsY), box432433theorem Continuous.fst (X Y : Set)434  requires spaceX : TopologicalSpace(X)435  requires spaceY : TopologicalSpace(Y)436  shows firstProjection(X.carrier, Y.carrier) : productSpace(X, Y) ⇒ X437proof438  have partsX := TopologicalSpace.parts with spaceX439  have partsY := TopologicalSpace.parts with spaceY440  have engine := Product.firstProjection.continuous with partsX, partsY441  have spaceP := productSpace.space with spaceX, spaceY442  have shifted : ContinuousMap(firstProjection(X.carrier, Y.carrier),443      TopologicalSpace.carrier(productSpace(X, Y)),444      TopologicalSpace.opens(productSpace(X, Y)), X.carrier, X.opens)445    rw [productSpace.carrier, productSpace.opens]446    exact engine447  exact Continuous.of_projections with spaceP, spaceX, shifted448449theorem Continuous.snd (X Y : Set)450  requires spaceX : TopologicalSpace(X)451  requires spaceY : TopologicalSpace(Y)452  shows secondProjection(X.carrier, Y.carrier) : productSpace(X, Y) ⇒ Y453proof454  have partsX := TopologicalSpace.parts with spaceX455  have partsY := TopologicalSpace.parts with spaceY456  have engine := Product.secondProjection.continuous with partsX, partsY457  have spaceP := productSpace.space with spaceX, spaceY458  have shifted : ContinuousMap(secondProjection(X.carrier, Y.carrier),459      TopologicalSpace.carrier(productSpace(X, Y)),460      TopologicalSpace.opens(productSpace(X, Y)), Y.carrier, Y.opens)461    rw [productSpace.carrier, productSpace.opens]462    exact engine463  exact Continuous.of_projections with spaceP, spaceY, shifted464465instance Hausdorff.prod (X Y : Set)466  requires spaceX : TopologicalSpace(X)467  requires spaceY : TopologicalSpace(Y)468  requires hausdorffX : Hausdorff(X)469  requires hausdorffY : Hausdorff(Y)470  shows Hausdorff(productSpace(X, Y))471proof472  have partsX := TopologicalSpace.parts with spaceX473  have partsY := TopologicalSpace.parts with spaceY474  have piecesX := Hausdorff.parts with hausdorffX475  have piecesY := Hausdorff.parts with hausdorffY476  unfold productSpace477  have product := Separation.IsHausdorff.product with partsX, partsY, piecesX, piecesY478  exact Hausdorff.of_mk with product479480theorem Compact.prod (X Y A B : Set)481  requires spaceX : TopologicalSpace(X)482  requires spaceY : TopologicalSpace(Y)483  requires compactA : Compact(X, A)484  requires compactB : Compact(Y, B)485  shows Compact(productSpace(X, Y), A × B)486proof487  have partsX := TopologicalSpace.parts with spaceX488  have partsY := TopologicalSpace.parts with spaceY489  have piecesA := Compact.parts with compactA490  have piecesB := Compact.parts with compactB491  have product := Tube.IsCompact.product with partsX, partsY, piecesA, piecesB492  unfold productSpace493  have topology := productTopology.topology with partsX, partsY494  exact Compact.of_mk with topology, product495496-- The real line: Hausdorff, with closed intervals closed and compact497-- (Heine–Borel), closed rectangles compact in the plane, and ε–δ498-- continuity the continuity of the line into itself.499instance realLine.hausdorff500  shows Hausdorff(realLine)501proof502  unfold realLine503  exact Hausdorff.of_mk with realTopology.hausdorff504505instance Closed.interval (A B : Real)506  shows Closed(realLine, closedInterval(A, B))507proof508  unfold realLine509  exact Closed.of_mk with realTopology.topology, (closedInterval.closed at A, B)510511theorem Compact.interval (A B : Real)512  requires ordered : A ≤ B513  shows Compact(realLine, closedInterval(A, B))514proof515  unfold realLine516  have compact := closedInterval.compact with ordered517  exact Compact.of_mk with realTopology.topology, compact518519theorem Compact.rectangle (A B C D : Real)520  requires orderedX : A ≤ B521  requires orderedY : C ≤ D522  shows Compact(plane, closedInterval(A, B) × closedInterval(C, D))523proof524  unfold plane525  have compact := closedRectangle.compact with orderedX, orderedY526  exact Compact.of_mk with planeTopology.topology, compact527528theorem Continuous.iff_real_line (f : Set)529  shows Continuous(f) ↔ f : realLine ⇒ realLine530proof531  have characterization := Continuous.continuous_map at f532  constructor533  . intro continuous534    have engine := characterization.forward with continuous535    unfold realLine536    have topology := realTopology.topology537    exact Continuous.of_parts with *538  . intro continuous539    have engine := Continuous.parts with continuous540    rw [realLine.carrier, realLine.opens] at engine541    exact characterization.backward with engine542