Grace/Cumulus/Topology/Space.g17

Open in Workbench Download source

Imports

Set

Declarations

Source

1-- Topological spaces: a topology on a set is a family of subsets closed2-- under arbitrary unions and binary intersections and containing the whole3-- set; closed sets, interior, and closure, with their basic laws4-- 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.Space10import Set1112predicate IsTopology (X T : Set) :=13  (T ⊆ 𝒫(X)) ∧ X ∈ T ∧14  (∀ S, S ⊆ T → ⋃(S) ∈ T) ∧15  (∀ U ∈ T, ∀ V ∈ T, U ∩ V ∈ T)1617-- The members of T are the open sets; a closed set is a subset of X whose18-- complement in X is open.19predicate IsClosed (X T C : Set) := (C ⊆ X) ∧ complement(X, C) ∈ T2021theorem IsTopology.subset (X T U : Set)22  requires topology : IsTopology(X, T)23  requires hU : U ∈ T24  shows U ⊆ X25proof26  obtain ⟨subsets, whole, unions, intersections⟩ := topology27  have member := subsets with U, hU28  exact powerset.membership_iff.forward with member2930theorem IsTopology.whole (X T : Set)31  requires topology : IsTopology(X, T)32  shows X ∈ T33proof34  obtain ⟨subsets, whole, unions, intersections⟩ := topology35  exact whole3637theorem IsTopology.union (X T S : Set)38  requires topology : IsTopology(X, T)39  requires hS : S ⊆ T40  shows ⋃(S) ∈ T41proof42  obtain ⟨subsets, whole, unions, intersections⟩ := topology43  exact unions with S, hS4445theorem IsTopology.intersection2 (X T U V : Set)46  requires topology : IsTopology(X, T)47  requires hU : U ∈ T48  requires hV : V ∈ T49  shows U ∩ V ∈ T50proof51  obtain ⟨subsets, whole, unions, intersections⟩ := topology52  exact intersections with U, hU, V, hV5354theorem IsTopology.empty (X T : Set)55  requires topology : IsTopology(X, T)56  shows ∅ ∈ T57proof58  have inside := empty.subset at T59  have member := IsTopology.union with topology, inside60  rwa union.empty at member6162theorem IsTopology.union2 (X T U V : Set)63  requires topology : IsTopology(X, T)64  requires hU : U ∈ T65  requires hV : V ∈ T66  shows U ∪ V ∈ T67proof68  have inside : {U, V} ⊆ T69    intros W hW70    have split := pair.membership.forward with hW71    cases split with isU | isV72    . rw isU73      exact hU74    . rw isV75      exact hV76  have member := IsTopology.union with topology, inside77  rwa union.pair at member7879-- Closed sets8081theorem IsClosed.whole (X T : Set)82  requires topology : IsTopology(X, T)83  shows IsClosed(X, T, X)84proof85  constructor86  . exact Subset.reflexive at X87  . rw complement.self88    exact IsTopology.empty with topology8990theorem IsClosed.empty (X T : Set)91  requires topology : IsTopology(X, T)92  shows IsClosed(X, T, ∅)93proof94  constructor95  . exact empty.subset at X96  . rw complement.empty97    exact IsTopology.whole with topology9899theorem IsClosed.complement_open (X T C : Set)100  requires closed : IsClosed(X, T, C)101  shows complement(X, C) ∈ T102proof103  exact closed.right104105theorem Open.complement_closed (X T U : Set)106  requires topology : IsTopology(X, T)107  requires hU : U ∈ T108  shows IsClosed(X, T, complement(X, U))109proof110  have inside := IsTopology.subset with topology, hU111  constructor112  . exact complement.subset at X, U113  . have double := complement.complement with inside114    rwa double115116theorem IsClosed.union2 (X T C D : Set)117  requires topology : IsTopology(X, T)118  requires hC : IsClosed(X, T, C)119  requires hD : IsClosed(X, T, D)120  shows IsClosed(X, T, C ∪ D)121proof122  constructor123  . exact union2.subset with hC.left, hD.left124  . rw complement.union2_distrib125    exact IsTopology.intersection2 with topology, hC.right, hD.right126127theorem IsClosed.intersection2 (X T C D : Set)128  requires topology : IsTopology(X, T)129  requires hC : IsClosed(X, T, C)130  requires hD : IsClosed(X, T, D)131  shows IsClosed(X, T, C ∩ D)132proof133  constructor134  . exact Subset.transitive with (intersection.subset_left at C, D), hC.left135  . rw complement.intersection_distrib136    exact IsTopology.union2 with topology, hC.right, hD.right137138theorem IsClosed.family_intersection (X T S : Set)139  requires topology : IsTopology(X, T)140  requires nonempty : Nonempty(S)141  requires closed : ∀ C ∈ S, IsClosed(X, T, C)142  shows IsClosed(X, T, ⋂(S))143proof144  obtain ⟨C, hC⟩ := nonempty145  have inhabited : Nonempty(S) := ⟨C, hC⟩146  constructor147  . have below := familyIntersection.subset_of_member with hC148    have closedC := closed with C, hC149    exact Subset.transitive with below, closedC.left150  . have demorgan := complements.intersection at X, S with inhabited151    rw demorgan152    apply IsTopology.union with topology153    intros V hV154    obtain ⟨D, hD, shape⟩ := complements.membership.forward with hV155    rw ← shape156    have closedD := closed with D, hD157    have openD := closedD.right158    unfold complement at openD159    exact openD160161-- Interior: the largest open set inside A.162163def openSubsets (T A : Set) : Set := { U ∈ T | U ⊆ A }164def interiorIn (T A : Set) : Set := ⋃(openSubsets(T, A))165166theorem interiorIn.open (X T A : Set)167  requires topology : IsTopology(X, T)168  shows interiorIn(T, A) ∈ T169proof170  unfold interiorIn171  apply IsTopology.union with topology172  intros U hU173  have parts := openSubsets.membership.forward with hU174  exact parts.left175176theorem interiorIn.subset (T A : Set)177  shows interiorIn(T, A) ⊆ A178proof179  unfold interiorIn180  apply union.subset181  intros U hU182  have parts := openSubsets.membership.forward with hU183  exact parts.right184185theorem interiorIn.greatest (T A U : Set)186  requires hU : U ∈ T187  requires inside : U ⊆ A188  shows U ⊆ interiorIn(T, A)189proof190  have member : U ∈ openSubsets(T, A) := openSubsets.membership.backward with ⟨hU, inside⟩191  unfold interiorIn192  exact union.subset_of_member with member193194theorem interiorIn.of_open (T U : Set)195  requires hU : U ∈ T196  shows interiorIn(T, U) = U197proof198  apply Subset.antisymmetric199  . exact interiorIn.subset at T, U200  . exact interiorIn.greatest with hU, (Subset.reflexive at U)201202theorem interiorIn.monotone (X T A B : Set)203  requires topology : IsTopology(X, T)204  requires hAB : A ⊆ B205  shows interiorIn(T, A) ⊆ interiorIn(T, B)206proof207  have isOpen := interiorIn.open at X, T, A with topology208  have inside := Subset.transitive with (interiorIn.subset at T, A), hAB209  exact interiorIn.greatest with isOpen, inside210211theorem interiorIn.idempotent (X T A : Set)212  requires topology : IsTopology(X, T)213  shows interiorIn(T, interiorIn(T, A)) = interiorIn(T, A)214proof215  exact interiorIn.of_open with (interiorIn.open at X, T, A with topology)216217theorem interiorIn.intersection2 (X T A B : Set)218  requires topology : IsTopology(X, T)219  shows interiorIn(T, A ∩ B) = interiorIn(T, A) ∩ interiorIn(T, B)220proof221  apply Subset.antisymmetric222  . apply intersection.greatest223    . exact interiorIn.monotone with topology, (intersection.subset_left at A, B)224    . exact interiorIn.monotone with topology, (intersection.subset_right at A, B)225  . have openA := interiorIn.open at X, T, A with topology226    have openB := interiorIn.open at X, T, B with topology227    have isOpen := IsTopology.intersection2 with topology, openA, openB228    have inside := intersection.monotone with (interiorIn.subset at T, A), (interiorIn.subset at T, B)229    exact interiorIn.greatest with isOpen, inside230231theorem Open.iff_interior (X T U : Set)232  requires topology : IsTopology(X, T)233  shows U ∈ T ↔ interiorIn(T, U) = U234proof235  constructor236  . intro hU237    exact interiorIn.of_open with hU238  . intro equal239    have isOpen := interiorIn.open at X, T, U with topology240    rwa equal at isOpen241242-- Closure: the smallest closed set around A.243244def closedSupersets (X T A : Set) : Set := { C ∈ 𝒫(X) | IsClosed(X, T, C) ∧ A ⊆ C }245def closure (X T A : Set) : Set := ⋂(closedSupersets(X, T, A))246247theorem closedSupersets.whole (X T A : Set)248  requires topology : IsTopology(X, T)249  requires hA : A ⊆ X250  shows X ∈ closedSupersets(X, T, A)251proof252  exact closedSupersets.membership.backward with ⟨(powerset.membership_iff.backward with (Subset.reflexive at X)), (IsClosed.whole with topology), hA⟩253254theorem closure.closed (X T A : Set)255  requires topology : IsTopology(X, T)256  requires hA : A ⊆ X257  shows IsClosed(X, T, closure(X, T, A))258proof259  have whole := closedSupersets.whole with topology, hA260  have inhabited : Nonempty(closedSupersets(X, T, A)) := ⟨X, whole⟩261  unfold closure262  apply IsClosed.family_intersection with topology, inhabited263  intros C hC264  have parts := closedSupersets.membership.forward with hC265  have rest := parts.right266  exact rest.left267268theorem closure.contains (X T A : Set)269  requires topology : IsTopology(X, T)270  requires hA : A ⊆ X271  shows A ⊆ closure(X, T, A)272proof273  have whole := closedSupersets.whole with topology, hA274  have inhabited : Nonempty(closedSupersets(X, T, A)) := ⟨X, whole⟩275  unfold closure276  apply familyIntersection.greatest with inhabited277  intros C hC278  have parts := closedSupersets.membership.forward with hC279  have rest := parts.right280  exact rest.right281282theorem closure.least (X T A C : Set)283  requires closed : IsClosed(X, T, C)284  requires hAC : A ⊆ C285  shows closure(X, T, A) ⊆ C286proof287  have member : C ∈ closedSupersets(X, T, A)288    exact closedSupersets.membership.backward with ⟨(powerset.membership_iff.backward with closed.left), closed, hAC⟩289  unfold closure290  exact familyIntersection.subset_of_member with member291292theorem closure.subset (X T A : Set)293  requires topology : IsTopology(X, T)294  requires hA : A ⊆ X295  shows closure(X, T, A) ⊆ X296proof297  exact closure.least with (IsClosed.whole with topology), hA298299theorem closure.of_closed (X T C : Set)300  requires topology : IsTopology(X, T)301  requires closed : IsClosed(X, T, C)302  shows closure(X, T, C) = C303proof304  apply Subset.antisymmetric305  . exact closure.least with closed, (Subset.reflexive at C)306  . exact closure.contains with topology, closed.left307308theorem closure.monotone (X T A B : Set)309  requires topology : IsTopology(X, T)310  requires hB : B ⊆ X311  requires hAB : A ⊆ B312  shows closure(X, T, A) ⊆ closure(X, T, B)313proof314  have inside := Subset.transitive with hAB, (closure.contains with topology, hB)315  exact closure.least with inside316317theorem closure.idempotent (X T A : Set)318  requires topology : IsTopology(X, T)319  requires hA : A ⊆ X320  shows closure(X, T, closure(X, T, A)) = closure(X, T, A)321proof322  exact closure.of_closed with topology, (closure.closed with topology, hA)323324theorem closure.union2 (X T A B : Set)325  requires topology : IsTopology(X, T)326  requires hA : A ⊆ X327  requires hB : B ⊆ X328  shows closure(X, T, A ∪ B) = closure(X, T, A) ∪ closure(X, T, B)329proof330  have hAB := union2.subset with hA, hB331  apply Subset.antisymmetric332  . have closed := IsClosed.union2 with topology, (closure.closed with topology, hA), (closure.closed with topology, hB)333    have inside := union2.monotone with (closure.contains with topology, hA), (closure.contains with topology, hB)334    exact closure.least with closed, inside335  . apply union2.subset336    . exact closure.monotone with topology, hAB, (union2.subset_left at A, B)337    . exact closure.monotone with topology, hAB, (union2.subset_right at A, B)338339theorem IsClosed.iff_closure (X T C : Set)340  requires topology : IsTopology(X, T)341  requires hC : C ⊆ X342  shows IsClosed(X, T, C) ↔ closure(X, T, C) = C343proof344  constructor345  . intro closed346    exact closure.of_closed with topology, closed347  . intro equal348    have closed := closure.closed with topology, hC349    rwa equal at closed350351-- A point lies in the closure of A exactly when every open set around it352-- meets A.353theorem closure.membership (X T A x : Set)354  requires topology : IsTopology(X, T)355  requires hA : A ⊆ X356  shows x ∈ closure(X, T, A) ↔ x ∈ X ∧ (∀ U ∈ T, x ∈ U → Nonempty(U ∩ A))357proof358  constructor359  . intro hx360    have inside := closure.subset with topology, hA361    have inX := inside with x, hx362    refine ⟨inX, ?_⟩363    intros U hU hxU364    by_contra empty365    have missing : A ⊆ complement(X, U)366      intros a ha367      apply complement.membership.backward368      refine ⟨(hA with a, ha), ?_⟩369      intro inU370      apply empty371      witness a372      exact intersection.membership.backward with ⟨inU, ha⟩373    have closed := Open.complement_closed with topology, hU374    have below := closure.least with missing375    have inside2 := below with x, hx376    have parts := complement.membership.forward with inside2377    exact parts.right with hxU378  . intro meets379    obtain ⟨inX, touches⟩ := meets380    by_contra outside381    have closed := closure.closed with topology, hA382    have hU := IsClosed.complement_open with closed383    have hxU : x ∈ complement(X, closure(X, T, A)) := complement.membership.backward with ⟨inX, outside⟩384    obtain ⟨a, ha⟩ := touches with complement(X, closure(X, T, A)), hU, hxU385    have parts := intersection.membership.forward with ha386    have contains := closure.contains with topology, hA387    have inClosure := contains with a, parts.right388    have away := complement.membership.forward with parts.left389    exact away.right with inClosure390391predicate IsDense (X T A : Set) := closure(X, T, A) = X392