Grace/Cumulus/Topology/Separation.g17

Open in Workbench Download source

Imports

Product · ClosureLaws · FiniteIntersection

Declarations

Source

1-- Separation axioms: T0 and T1 spaces below Hausdorff, points and finite2-- sets closed in T1 spaces, separation passes to subspaces and products,3-- and the regular and normal properties above Hausdorff4-- 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.Separation10import Product11import ClosureLaws12import FiniteIntersection1314-- T0: some open set tells two distinct points apart; T1: each of two15-- distinct points has an open set missing the other.16predicate T0Space (X T : Set) :=17  ∀ x ∈ X, ∀ y ∈ X, x ≠ y → ∃ U ∈ T, (x ∈ U ∧ ¬y ∈ U) ∨ (y ∈ U ∧ ¬x ∈ U)1819predicate IsT1Space (X T : Set) :=20  ∀ x ∈ X, ∀ y ∈ X, x ≠ y → ∃ U ∈ T, x ∈ U ∧ ¬y ∈ U2122theorem IsT1Space.t0 (X T : Set)23  requires t1 : IsT1Space(X, T)24  shows T0Space(X, T)25proof26  intros x hx y hy distinct27  obtain ⟨U, hU, hxU, away⟩ := t1 with x, hx, y, hy, distinct28  refine ⟨U, hU, ?_⟩29  left30  exact ⟨hxU, away⟩3132theorem IsHausdorff.t1 (X T : Set)33  requires hausdorff : IsHausdorff(X, T)34  shows IsT1Space(X, T)35proof36  intros x hx y hy distinct37  obtain ⟨U, hU, V, hV, hxU, hyV, disjoint⟩ := hausdorff with x, hx, y, hy, distinct38  have separated := Disjoint.iff.forward with disjoint39  refine ⟨U, hU, hxU, ?_⟩40  intro hyU41  exact separated with y, hyU, hyV4243theorem IsHausdorff.t0 (X T : Set)44  requires hausdorff : IsHausdorff(X, T)45  shows T0Space(X, T)46proof47  exact IsT1Space.t0 with (IsHausdorff.t1 with hausdorff)4849-- Points are closed in a T1 space, and that characterises T1.5051theorem IsT1Space.singleton_closed (X T x : Set)52  requires topology : IsTopology(X, T)53  requires t1 : IsT1Space(X, T)54  requires hx : x ∈ X55  shows IsClosed(X, T, {x})56proof57  constructor58  . intros z hz59    have same := singleton.membership.forward with hz60    rwa same61  . have awayOpen : awayFrom(T, x) ⊆ T62      intros V hV63      have parts := awayFrom.membership.forward with hV64      exact parts.left65    have isOpen := IsTopology.union with topology, awayOpen66    have equal : complement(X, {x}) = ⋃(awayFrom(T, x))67      ext y68      constructor69      . intro hy70        have parts := complement.membership.forward with hy71        have distinct : y ≠ x72          intro same73          apply parts.right74          rw same75          simp [singleton.membership]76        obtain ⟨V, hV, hyV, away⟩ := t1 with y, parts.left, x, hx, distinct77        have member : V ∈ awayFrom(T, x) := awayFrom.membership.backward with ⟨hV, away⟩78        exact union.contains with member, hyV79      . intro hy80        obtain ⟨V, hV, hyV⟩ := union.membership.forward with hy81        have parts := awayFrom.membership.forward with hV82        have inside := IsTopology.subset with topology, parts.left83        have hyX := inside with y, hyV84        apply complement.membership.backward85        refine ⟨hyX, ?_⟩86        intro same87        have equalYX := singleton.membership.forward with same88        apply parts.right89        rwa ← equalYX90    rwa equal9192theorem IsT1Space.of_singletons_closed (X T : Set)93  requires topology : IsTopology(X, T)94  requires closed : ∀ x ∈ X, IsClosed(X, T, {x})95  shows IsT1Space(X, T)96proof97  intros x hx y hy distinct98  have closedY := closed with y, hy99  have isOpen := IsClosed.complement_open with closedY100  refine ⟨complement(X, {y}), isOpen, ?_, ?_⟩101  . apply complement.membership.backward102    refine ⟨hx, ?_⟩103    intro same104    have equalXY := singleton.membership.forward with same105    exact distinct with equalXY106  . intro hyC107    have parts := complement.membership.forward with hyC108    apply parts.right109    simp [singleton.membership]110111theorem IsT1Space.iff_singletons_closed (X T : Set)112  requires topology : IsTopology(X, T)113  shows IsT1Space(X, T) ↔ ∀ x ∈ X, IsClosed(X, T, {x})114proof115  constructor116  . intros t1 x hx117    exact IsT1Space.singleton_closed with topology, t1, hx118  . intro closed119    exact IsT1Space.of_singletons_closed with topology, closed120121theorem IsT1Space.point_complement_open (X T x : Set)122  requires topology : IsTopology(X, T)123  requires t1 : IsT1Space(X, T)124  requires hx : x ∈ X125  shows complement(X, {x}) ∈ T126proof127  have closed := IsT1Space.singleton_closed with topology, t1, hx128  exact IsClosed.complement_open with closed129130-- Finite sets are closed in a T1 space: the support of a list of points131-- is a finite union of closed singletons.132theorem IsClosed.list_support (X T : Set) (xs : List(X))133  requires topology : IsTopology(X, T)134  requires t1 : IsT1Space(X, T)135  shows IsClosed(X, T, listSupport{X}(xs))136proof137  induction xs138  | List.nil =>139    rw listSupport.nil140    exact IsClosed.empty with topology141  | List.cons(a, tail) using ih =>142    have element : a ∈ X by assumption143    have closedPoint := IsT1Space.singleton_closed with topology, t1, element144    rw listSupport.cons145    unfold insert146    exact IsClosed.union2 with topology, closedPoint, ih147148theorem IsT1Space.finite_closed (X T F : Set)149  requires topology : IsTopology(X, T)150  requires t1 : IsT1Space(X, T)151  requires finite : Finite(F)152  requires hF : F ⊆ X153  shows IsClosed(X, T, F)154proof155  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite156  have weakened := List.weaken with hF157  have support := listSupport.subset with list158  have equal : listSupport{F}(xs) = F := Subset.antisymmetric with support, covers159  have carrier := listSupport.change_carrier with hF160  rw carrier at equal161  rw ← equal162  exact IsClosed.list_support with topology, t1163164theorem IsHausdorff.finite_closed (X T F : Set)165  requires topology : IsTopology(X, T)166  requires hausdorff : IsHausdorff(X, T)167  requires finite : Finite(F)168  requires hF : F ⊆ X169  shows IsClosed(X, T, F)170proof171  have t1 := IsHausdorff.t1 with hausdorff172  exact IsT1Space.finite_closed with topology, t1, finite, hF173174theorem IsT1Space.discrete (X : Set)175  shows IsT1Space(X, 𝒫(X))176proof177  exact IsHausdorff.t1 with (IsHausdorff.discrete at X)178179-- Separation passes to subspaces.180181theorem T0Space.subspace (X T A : Set)182  requires t0 : T0Space(X, T)183  requires hA : A ⊆ X184  shows T0Space(A, subspaceTopology(T, A))185proof186  intros x hx y hy distinct187  obtain ⟨U, hU, split⟩ := t0 with x, (hA with x, hx), y, (hA with y, hy), distinct188  have traced : U ∩ A ∈ subspaceTopology(T, A) := subspaceTopology.membership.backward with ⟨U, hU, rfl⟩189  refine ⟨U ∩ A, traced, ?_⟩190  cases split with xSide | ySide191  . left192    constructor193    . exact intersection.membership.backward with ⟨xSide.left, hx⟩194    . intro hyT195      have parts := intersection.membership.forward with hyT196      exact xSide.right with parts.left197  . right198    constructor199    . exact intersection.membership.backward with ⟨ySide.left, hy⟩200    . intro hxT201      have parts := intersection.membership.forward with hxT202      exact ySide.right with parts.left203204theorem IsT1Space.subspace (X T A : Set)205  requires t1 : IsT1Space(X, T)206  requires hA : A ⊆ X207  shows IsT1Space(A, subspaceTopology(T, A))208proof209  intros x hx y hy distinct210  obtain ⟨U, hU, hxU, away⟩ := t1 with x, (hA with x, hx), y, (hA with y, hy), distinct211  have traced : U ∩ A ∈ subspaceTopology(T, A) := subspaceTopology.membership.backward with ⟨U, hU, rfl⟩212  refine ⟨U ∩ A, traced, (intersection.membership.backward with ⟨hxU, hx⟩), ?_⟩213  intro hyT214  have parts := intersection.membership.forward with hyT215  exact away with parts.left216217theorem IsHausdorff.subspace (X T A : Set)218  requires hausdorff : IsHausdorff(X, T)219  requires hA : A ⊆ X220  shows IsHausdorff(A, subspaceTopology(T, A))221proof222  intros x hx y hy distinct223  obtain ⟨U, hU, V, hV, hxU, hyV, disjoint⟩ := hausdorff with x, (hA with x, hx), y, (hA with y, hy), distinct224  have tracedU : U ∩ A ∈ subspaceTopology(T, A) := subspaceTopology.membership.backward with ⟨U, hU, rfl⟩225  have tracedV : V ∩ A ∈ subspaceTopology(T, A) := subspaceTopology.membership.backward with ⟨V, hV, rfl⟩226  refine ⟨U ∩ A, tracedU, V ∩ A, tracedV, (intersection.membership.backward with ⟨hxU, hx⟩), (intersection.membership.backward with ⟨hyV, hy⟩), ?_⟩227  have below := intersection.subset_left at U, A228  have belowV := intersection.subset_left at V, A229  have first := Disjoint.of_subset_left with disjoint, below230  exact Disjoint.of_subset_right with first, belowV231232-- The product of two Hausdorff spaces is Hausdorff: distinct pairs differ233-- in some coordinate, and a box separates them there.234theorem IsHausdorff.product (X T Y S : Set)235  requires topologyX : IsTopology(X, T)236  requires topologyY : IsTopology(Y, S)237  requires hausdorffX : IsHausdorff(X, T)238  requires hausdorffY : IsHausdorff(Y, S)239  shows IsHausdorff(X × Y, productTopology(X, T, Y, S))240proof241  intros p hp q hq distinct242  obtain ⟨boundP, x1, hx1, y1, hy1, rfl⟩ := product.membership.forward with hp243  obtain ⟨boundQ, x2, hx2, y2, hy2, rfl⟩ := product.membership.forward with hq244  have wholeX := IsTopology.whole with topologyX245  have wholeY := IsTopology.whole with topologyY246  have split : x1 = x2 ∨ x1 ≠ x2 by tauto247  cases split with sameX | differentX248  . have differentY : y1 ≠ y2249      intro sameY250      apply distinct251      rw [sameX, sameY]252      rfl253    obtain ⟨U, hU, V, hV, hy1U, hy2V, disjoint⟩ := hausdorffY with y1, hy1, y2, hy2, differentY254    have boxU := productTopology.box with topologyX, topologyY, wholeX, hU255    have boxV := productTopology.box with topologyX, topologyY, wholeX, hV256    refine ⟨X × U, boxU, X × V, boxV, (product.pair with hx1, hy1U), (product.pair with hx2, hy2V), ?_⟩257    exact product.disjoint_of_right with disjoint258  . obtain ⟨U, hU, V, hV, hx1U, hx2V, disjoint⟩ := hausdorffX with x1, hx1, x2, hx2, differentX259    have boxU := productTopology.box with topologyX, topologyY, hU, wholeY260    have boxV := productTopology.box with topologyX, topologyY, hV, wholeY261    refine ⟨U × Y, boxU, V × Y, boxV, (product.pair with hx1U, hy1), (product.pair with hx2V, hy2), ?_⟩262    exact product.disjoint_of_left with disjoint263264-- Regular: a point and a closed set missing it have disjoint open265-- neighbourhoods; normal: two disjoint closed sets do.266predicate RegularSpace (X T : Set) :=267  ∀ x ∈ X, ∀ C, IsClosed(X, T, C) → ¬x ∈ C →268    ∃ U ∈ T, ∃ V ∈ T, x ∈ U ∧ C ⊆ V ∧ Disjoint(U, V)269270predicate NormalSpace (X T : Set) :=271  ∀ C, IsClosed(X, T, C) → ∀ D, IsClosed(X, T, D) → Disjoint(C, D) →272    ∃ U ∈ T, ∃ V ∈ T, C ⊆ U ∧ D ⊆ V ∧ Disjoint(U, V)273274theorem RegularSpace.hausdorff (X T : Set)275  requires topology : IsTopology(X, T)276  requires t1 : IsT1Space(X, T)277  requires regular : RegularSpace(X, T)278  shows IsHausdorff(X, T)279proof280  intros x hx y hy distinct281  have closedY := IsT1Space.singleton_closed with topology, t1, hy282  have away : ¬x ∈ {y}283    intro same284    have equalXY := singleton.membership.forward with same285    exact distinct with equalXY286  obtain ⟨U, hU, V, hV, hxU, inside, disjoint⟩ := regular with x, hx, {y}, closedY, away287  have self : y ∈ {y} by simp [singleton.membership]288  have hyV := inside with y, self289  exact ⟨U, hU, V, hV, hxU, hyV, disjoint⟩290291theorem NormalSpace.regular (X T : Set)292  requires topology : IsTopology(X, T)293  requires t1 : IsT1Space(X, T)294  requires normal : NormalSpace(X, T)295  shows RegularSpace(X, T)296proof297  intros x hx C closedC away298  have closedX := IsT1Space.singleton_closed with topology, t1, hx299  have disjoint : Disjoint({x}, C)300    apply Disjoint.iff.backward301    intros z hz hzC302    have same := singleton.membership.forward with hz303    apply away304    rwa same at hzC305  obtain ⟨U, hU, V, hV, inside, insideC, separated⟩ := normal with {x}, closedX, C, closedC, disjoint306  have self : x ∈ {x} by simp [singleton.membership]307  have hxU := inside with x, self308  exact ⟨U, hU, V, hV, hxU, insideC, separated⟩309310theorem NormalSpace.hausdorff (X T : Set)311  requires topology : IsTopology(X, T)312  requires t1 : IsT1Space(X, T)313  requires normal : NormalSpace(X, T)314  shows IsHausdorff(X, T)315proof316  have regular := NormalSpace.regular with topology, t1, normal317  exact RegularSpace.hausdorff with topology, t1, regular318319-- In the discrete topology every set is open, so closed sets separate320-- themselves.321theorem NormalSpace.discrete (X : Set)322  shows NormalSpace(X, 𝒫(X))323proof324  intros C closedC D closedD disjoint325  have openC : C ∈ 𝒫(X) := powerset.membership_iff.backward with closedC.left326  have openD : D ∈ 𝒫(X) := powerset.membership_iff.backward with closedD.left327  exact ⟨C, openC, D, openD, (Subset.reflexive at C), (Subset.reflexive at D), disjoint⟩328329theorem RegularSpace.discrete (X : Set)330  shows RegularSpace(X, 𝒫(X))331proof332  have topology := discreteTopology at X333  have t1 := IsT1Space.discrete at X334  have normal := NormalSpace.discrete at X335  exact NormalSpace.regular with topology, t1, normal336337-- In a T1 space every neighbourhood of a limit point of A meets A away338-- from any finite set of points.339theorem IsT1Space.limit_point_avoids (X T A x F : Set)340  requires topology : IsTopology(X, T)341  requires t1 : IsT1Space(X, T)342  requires limit : x ∈ limitPoints(X, T, A)343  requires finite : Finite(F)344  requires hF : F ⊆ X345  requires away : ¬x ∈ F346  shows ∀ U ∈ T, x ∈ U → Nonempty(U ∩ (A ∖ F))347proof348  intros U hU hxU349  have parts := limitPoints.membership.forward with limit350  have closedF := IsT1Space.finite_closed with topology, t1, finite, hF351  have openF := IsClosed.complement_open with closedF352  have hxC : x ∈ complement(X, F) := complement.membership.backward with ⟨parts.left, away⟩353  have openBoth := IsTopology.intersection2 with topology, hU, openF354  have inBoth : x ∈ U ∩ complement(X, F) := intersection.membership.backward with ⟨hxU, hxC⟩355  obtain ⟨a, ha⟩ := parts.right with U ∩ complement(X, F), openBoth, inBoth356  have inner := intersection.membership.forward with ha357  have inU := intersection.membership.forward with inner.left358  have outside := complement.membership.forward with inU.right359  have inA := difference.singleton_membership.forward with inner.right360  witness a361  apply intersection.membership.backward362  refine ⟨inU.left, ?_⟩363  exact difference.membership.backward with ⟨inA.left, outside.right⟩364