-- Examples and constructions: the discrete and indiscrete topologies, the -- subspace topology, and the Hausdorff separation property -- Part of Cumulus, the Grace17 mathematics library. -- Copyright (c) 2026 Grant Passmore. -- Released under the Apache License 2.0. See LICENSE in the repository root. -- Authors: Grant Passmore module Grace.Cumulus.Topology.Subspace import Compact theorem discreteTopology (X : Set) shows IsTopology(X, 𝒫(X)) proof constructor . exact Subset.reflexive at 𝒫(X) . constructor . exact powerset.membership_iff.backward with (Subset.reflexive at X) . constructor . intros S hS apply powerset.membership_iff.backward apply union.subset intros U hU exact powerset.membership_iff.forward with (hS with U, hU) . intros U hU V hV apply powerset.membership_iff.backward have inside := powerset.membership_iff.forward with hU exact Subset.transitive with (intersection.subset_left at U, V), inside theorem indiscreteTopology (X : Set) shows IsTopology(X, {∅, X}) proof constructor . intros U hU have split := pair.membership.forward with hU apply powerset.membership_iff.backward cases split with isEmpty | isWhole . rw isEmpty exact empty.subset . rw isWhole exact Subset.reflexive . constructor . apply pair.membership.backward right rfl . constructor . intros S hS have split : X ∈ S ∨ ¬X ∈ S by tauto cases split with inside | outside . have equal : ⋃(S) = X apply Subset.antisymmetric . apply union.subset intros U hU have cases := pair.membership.forward with (hS with U, hU) cases cases with isEmpty | isWhole . rw isEmpty exact empty.subset . rw isWhole exact Subset.reflexive . exact union.subset_of_member with inside rw equal apply pair.membership.backward right rfl . have equal : ⋃(S) = ∅ apply Subset.antisymmetric . apply union.subset intros U hU have cases := pair.membership.forward with (hS with U, hU) cases cases with isEmpty | isWhole . rw isEmpty exact Subset.reflexive . exfalso rw isWhole at hU exact outside with hU . exact empty.subset at ⋃(S) rw equal apply pair.membership.backward left rfl . intros U hU V hV have splitU := pair.membership.forward with hU cases splitU with emptyU | wholeU . rw [emptyU, intersection.left_empty] apply pair.membership.backward left rfl . have splitV := pair.membership.forward with hV cases splitV with emptyV | wholeV . rw [emptyV, intersection.right_empty] apply pair.membership.backward left rfl . rw [wholeU, wholeV, intersection.idempotent] apply pair.membership.backward right rfl -- The subspace topology on A ⊆ X: traces of the open sets of X. def subspaceTopology (T A : Set) : Set := { U ∩ A | U ∈ T } def tracedBy (T A S : Set) : Set := { U ∈ T | U ∩ A ∈ S } theorem subspaceTopology.topology (X T A : Set) requires topology : IsTopology(X, T) requires hA : A ⊆ X shows IsTopology(A, subspaceTopology(T, A)) proof constructor . intros V hV obtain ⟨U, hU, shape⟩ := subspaceTopology.membership.forward with hV apply powerset.membership_iff.backward rw ← shape exact intersection.subset_right . constructor . apply subspaceTopology.membership.backward refine ⟨X, (IsTopology.whole with topology), ?_⟩ exact intersection.eq_right_of_subset with hA . constructor . intros S hS have tracedOpen : tracedBy(T, A, S) ⊆ T intros U hU have parts := tracedBy.membership.forward with hU exact parts.left have isOpen := IsTopology.union with topology, tracedOpen apply subspaceTopology.membership.backward refine ⟨⋃(tracedBy(T, A, S)), isOpen, ?_⟩ ext x constructor . intro hx have parts := intersection.membership.forward with hx obtain ⟨U, hU, hxU⟩ := union.membership.forward with parts.left have traced := tracedBy.membership.forward with hU have inTrace : x ∈ U ∩ A := intersection.membership.backward with ⟨hxU, parts.right⟩ exact union.contains with traced.right, inTrace . intro hx obtain ⟨V, hV, hxV⟩ := union.membership.forward with hx obtain ⟨U, hU, shape⟩ := subspaceTopology.membership.forward with (hS with V, hV) rw ← shape at hxV have parts := intersection.membership.forward with hxV have traced : U ∈ tracedBy(T, A, S) apply tracedBy.membership.backward rw shape exact ⟨hU, hV⟩ apply intersection.membership.backward exact ⟨(union.contains with traced, parts.left), parts.right⟩ . intros V hV W hW obtain ⟨U, hU, shapeV⟩ := subspaceTopology.membership.forward with hV obtain ⟨U2, hU2, shapeW⟩ := subspaceTopology.membership.forward with hW apply subspaceTopology.membership.backward refine ⟨U ∩ U2, (IsTopology.intersection2 with topology, hU, hU2), ?_⟩ rw [← shapeV, ← shapeW] ext x simp [intersection.membership] -- Hausdorff spaces: distinct points have disjoint open neighbourhoods. predicate IsHausdorff (X T : Set) := ∀ x ∈ X, ∀ y ∈ X, x ≠ y → ∃ U ∈ T, ∃ V ∈ T, x ∈ U ∧ y ∈ V ∧ Disjoint(U, V) theorem IsHausdorff.discrete (X : Set) shows IsHausdorff(X, 𝒫(X)) proof intros x hx y hy distinct have singletonX : {x} ⊆ X intros z hz have same := singleton.membership.forward with hz rwa same have singletonY : {y} ⊆ X intros z hz have same := singleton.membership.forward with hz rwa same refine ⟨{x}, (powerset.membership_iff.backward with singletonX), {y}, (powerset.membership_iff.backward with singletonY), ?_, ?_, ?_⟩ . simp [singleton.membership] . simp [singleton.membership] . apply Disjoint.iff.backward intros z hz hz2 have sameX := singleton.membership.forward with hz have sameY := singleton.membership.forward with hz2 apply distinct rw [← sameX, ← sameY] rfl def awayFrom (T x : Set) : Set := { V ∈ T | ¬x ∈ V } -- In a Hausdorff space every point is closed. theorem IsHausdorff.singleton_closed (X T x : Set) requires topology : IsTopology(X, T) requires hausdorff : IsHausdorff(X, T) requires hx : x ∈ X shows IsClosed(X, T, {x}) proof constructor . intros z hz have same := singleton.membership.forward with hz rwa same . have awayOpen : awayFrom(T, x) ⊆ T intros V hV have parts := awayFrom.membership.forward with hV exact parts.left have isOpen := IsTopology.union with topology, awayOpen have equal : complement(X, {x}) = ⋃(awayFrom(T, x)) ext y constructor . intro hy have parts := complement.membership.forward with hy have distinct : x ≠ y intro same apply parts.right rw ← same simp [singleton.membership] obtain ⟨U, hU, V, hV, hxU, hyV, disjoint⟩ := hausdorff with x, hx, y, parts.left, distinct have separated := Disjoint.iff.forward with disjoint have away : V ∈ awayFrom(T, x) apply awayFrom.membership.backward refine ⟨hV, ?_⟩ intro hxV exact separated with x, hxU, hxV exact union.contains with away, hyV . intro hy obtain ⟨V, hV, hyV⟩ := union.membership.forward with hy have parts := awayFrom.membership.forward with hV have inside := IsTopology.subset with topology, parts.left have hyX := inside with y, hyV apply complement.membership.backward refine ⟨hyX, ?_⟩ intro same have equalXY := singleton.membership.forward with same apply parts.right rwa ← equalXY rwa equal