Grace/Cumulus/Topology/Subspace.g17

Open in Workbench Download source

Imports

Compact

Declarations

Source

1-- Examples and constructions: the discrete and indiscrete topologies, the2-- subspace topology, and the Hausdorff separation property3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Topology.Subspace9import Compact1011theorem discreteTopology (X : Set)12  shows IsTopology(X, 𝒫(X))13proof14  constructor15  . exact Subset.reflexive at 𝒫(X)16  . constructor17    . exact powerset.membership_iff.backward with (Subset.reflexive at X)18    . constructor19      . intros S hS20        apply powerset.membership_iff.backward21        apply union.subset22        intros U hU23        exact powerset.membership_iff.forward with (hS with U, hU)24      . intros U hU V hV25        apply powerset.membership_iff.backward26        have inside := powerset.membership_iff.forward with hU27        exact Subset.transitive with (intersection.subset_left at U, V), inside2829theorem indiscreteTopology (X : Set)30  shows IsTopology(X, {∅, X})31proof32  constructor33  . intros U hU34    have split := pair.membership.forward with hU35    apply powerset.membership_iff.backward36    cases split with isEmpty | isWhole37    . rw isEmpty38      exact empty.subset39    . rw isWhole40      exact Subset.reflexive41  . constructor42    . apply pair.membership.backward43      right44      rfl45    . constructor46      . intros S hS47        have split : X ∈ S ∨ ¬X ∈ S by tauto48        cases split with inside | outside49        . have equal : ⋃(S) = X50            apply Subset.antisymmetric51            . apply union.subset52              intros U hU53              have cases := pair.membership.forward with (hS with U, hU)54              cases cases with isEmpty | isWhole55              . rw isEmpty56                exact empty.subset57              . rw isWhole58                exact Subset.reflexive59            . exact union.subset_of_member with inside60          rw equal61          apply pair.membership.backward62          right63          rfl64        . have equal : ⋃(S) = ∅65            apply Subset.antisymmetric66            . apply union.subset67              intros U hU68              have cases := pair.membership.forward with (hS with U, hU)69              cases cases with isEmpty | isWhole70              . rw isEmpty71                exact Subset.reflexive72              . exfalso73                rw isWhole at hU74                exact outside with hU75            . exact empty.subset at ⋃(S)76          rw equal77          apply pair.membership.backward78          left79          rfl80      . intros U hU V hV81        have splitU := pair.membership.forward with hU82        cases splitU with emptyU | wholeU83        . rw [emptyU, intersection.left_empty]84          apply pair.membership.backward85          left86          rfl87        . have splitV := pair.membership.forward with hV88          cases splitV with emptyV | wholeV89          . rw [emptyV, intersection.right_empty]90            apply pair.membership.backward91            left92            rfl93          . rw [wholeU, wholeV, intersection.idempotent]94            apply pair.membership.backward95            right96            rfl9798-- The subspace topology on A ⊆ X: traces of the open sets of X.99def subspaceTopology (T A : Set) : Set := { U ∩ A | U ∈ T }100def tracedBy (T A S : Set) : Set := { U ∈ T | U ∩ A ∈ S }101102theorem subspaceTopology.topology (X T A : Set)103  requires topology : IsTopology(X, T)104  requires hA : A ⊆ X105  shows IsTopology(A, subspaceTopology(T, A))106proof107  constructor108  . intros V hV109    obtain ⟨U, hU, shape⟩ := subspaceTopology.membership.forward with hV110    apply powerset.membership_iff.backward111    rw ← shape112    exact intersection.subset_right113  . constructor114    . apply subspaceTopology.membership.backward115      refine ⟨X, (IsTopology.whole with topology), ?_⟩116      exact intersection.eq_right_of_subset with hA117    . constructor118      . intros S hS119        have tracedOpen : tracedBy(T, A, S) ⊆ T120          intros U hU121          have parts := tracedBy.membership.forward with hU122          exact parts.left123        have isOpen := IsTopology.union with topology, tracedOpen124        apply subspaceTopology.membership.backward125        refine ⟨⋃(tracedBy(T, A, S)), isOpen, ?_⟩126        ext x127        constructor128        . intro hx129          have parts := intersection.membership.forward with hx130          obtain ⟨U, hU, hxU⟩ := union.membership.forward with parts.left131          have traced := tracedBy.membership.forward with hU132          have inTrace : x ∈ U ∩ A := intersection.membership.backward with ⟨hxU, parts.right⟩133          exact union.contains with traced.right, inTrace134        . intro hx135          obtain ⟨V, hV, hxV⟩ := union.membership.forward with hx136          obtain ⟨U, hU, shape⟩ := subspaceTopology.membership.forward with (hS with V, hV)137          rw ← shape at hxV138          have parts := intersection.membership.forward with hxV139          have traced : U ∈ tracedBy(T, A, S)140            apply tracedBy.membership.backward141            rw shape142            exact ⟨hU, hV⟩143          apply intersection.membership.backward144          exact ⟨(union.contains with traced, parts.left), parts.right⟩145      . intros V hV W hW146        obtain ⟨U, hU, shapeV⟩ := subspaceTopology.membership.forward with hV147        obtain ⟨U2, hU2, shapeW⟩ := subspaceTopology.membership.forward with hW148        apply subspaceTopology.membership.backward149        refine ⟨U ∩ U2, (IsTopology.intersection2 with topology, hU, hU2), ?_⟩150        rw [← shapeV, ← shapeW]151        ext x152        simp [intersection.membership]153154-- Hausdorff spaces: distinct points have disjoint open neighbourhoods.155predicate IsHausdorff (X T : Set) :=156  ∀ x ∈ X, ∀ y ∈ X, x ≠ y → ∃ U ∈ T, ∃ V ∈ T, x ∈ U ∧ y ∈ V ∧ Disjoint(U, V)157158theorem IsHausdorff.discrete (X : Set)159  shows IsHausdorff(X, 𝒫(X))160proof161  intros x hx y hy distinct162  have singletonX : {x} ⊆ X163    intros z hz164    have same := singleton.membership.forward with hz165    rwa same166  have singletonY : {y} ⊆ X167    intros z hz168    have same := singleton.membership.forward with hz169    rwa same170  refine ⟨{x}, (powerset.membership_iff.backward with singletonX), {y}, (powerset.membership_iff.backward with singletonY), ?_, ?_, ?_⟩171  . simp [singleton.membership]172  . simp [singleton.membership]173  . apply Disjoint.iff.backward174    intros z hz hz2175    have sameX := singleton.membership.forward with hz176    have sameY := singleton.membership.forward with hz2177    apply distinct178    rw [← sameX, ← sameY]179    rfl180181def awayFrom (T x : Set) : Set := { V ∈ T | ¬x ∈ V }182183-- In a Hausdorff space every point is closed.184theorem IsHausdorff.singleton_closed (X T x : Set)185  requires topology : IsTopology(X, T)186  requires hausdorff : IsHausdorff(X, T)187  requires hx : x ∈ X188  shows IsClosed(X, T, {x})189proof190  constructor191  . intros z hz192    have same := singleton.membership.forward with hz193    rwa same194  . have awayOpen : awayFrom(T, x) ⊆ T195      intros V hV196      have parts := awayFrom.membership.forward with hV197      exact parts.left198    have isOpen := IsTopology.union with topology, awayOpen199    have equal : complement(X, {x}) = ⋃(awayFrom(T, x))200      ext y201      constructor202      . intro hy203        have parts := complement.membership.forward with hy204        have distinct : x ≠ y205          intro same206          apply parts.right207          rw ← same208          simp [singleton.membership]209        obtain ⟨U, hU, V, hV, hxU, hyV, disjoint⟩ := hausdorff with x, hx, y, parts.left, distinct210        have separated := Disjoint.iff.forward with disjoint211        have away : V ∈ awayFrom(T, x)212          apply awayFrom.membership.backward213          refine ⟨hV, ?_⟩214          intro hxV215          exact separated with x, hxU, hxV216        exact union.contains with away, hyV217      . intro hy218        obtain ⟨V, hV, hyV⟩ := union.membership.forward with hy219        have parts := awayFrom.membership.forward with hV220        have inside := IsTopology.subset with topology, parts.left221        have hyX := inside with y, hyV222        apply complement.membership.backward223        refine ⟨hyX, ?_⟩224        intro same225        have equalXY := singleton.membership.forward with same226        apply parts.right227        rwa ← equalXY228    rwa equal229