Mathlib.Topology.Separation.Regular

RegularSpace structure

(X : Type u) [TopologicalSpace X]

Full source

/-- A topological space is called a *regular space* if for any closed set `s` and `a ∉ s`, there
exist disjoint open sets `U ⊇ s` and `V ∋ a`. We formulate this condition in terms of `Disjoint`ness
of filters `𝓝ˢ s` and `𝓝 a`. -/
@[mk_iff]
class RegularSpace (X : Type u) [TopologicalSpace X] : Prop where
  /-- If `a` is a point that does not belong to a closed set `s`, then `a` and `s` admit disjoint
  neighborhoods. -/
  regular : ∀ {s : Set X} {a}, IsClosed s → a ∉ s → Disjoint (𝓝ˢ s) (𝓝 a)

Regular Space

Informal description

A topological space $ X $ is called a *regular space* if for any closed set $ C \subseteq X $ and any point $ x \notin C $, there exist disjoint open sets $ U $ and $ V $ such that $ C \subseteq U $ and $ x \in V $. This condition is formulated in terms of the disjointness of the neighborhood filter of $ x $ and the neighborhood filter of $ C $.

regularSpace_TFAE theorem

 (X : Type u) [TopologicalSpace X] :
  List.TFAE
    [RegularSpace X, ∀ (s : Set X) x, x ∉ closure s → Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s,
      ∀ (x : X) (s : Set X), s ∈ 𝓝 x → ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s, ∀ x : X, (𝓝 x).lift' closure ≤ 𝓝 x,
      ∀ x : X, (𝓝 x).lift' closure = 𝓝 x]

Full source

theorem regularSpace_TFAE (X : Type u) [TopologicalSpace X] :
    List.TFAE [RegularSpace X,
      ∀ (s : Set X) x, x ∉ closure s → Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s,
      ∀ (x : X) (s : Set X), s ∈ 𝓝 x → ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s,
      ∀ x : X, (𝓝 x).lift' closure ≤ 𝓝 x,
      ∀ x : X , (𝓝 x).lift' closure = 𝓝 x] := by
  tfae_have 1 ↔ 5 := by
    rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_swap]
    simp only [isClosed_compl_iff, mem_compl_iff, Classical.not_not, @and_comm (_ ∈ _),
      (nhds_basis_opens _).lift'_closure.le_basis_iff (nhds_basis_opens _), and_imp,
      (nhds_basis_opens _).disjoint_iff_right, exists_prop, ← subset_interior_iff_mem_nhdsSet,
      interior_compl, compl_subset_compl]
  tfae_have 5 → 6 := fun h a => (h a).antisymm (𝓝 _).le_lift'_closure
  tfae_have 6 → 4
  | H, a, s, hs => by
    rw [← H] at hs
    rcases (𝓝 a).basis_sets.lift'_closure.mem_iff.mp hs with ⟨U, hU, hUs⟩
    exact ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, hUs⟩
  tfae_have 4 → 2
  | H, s, a, ha => by
    have ha' : sᶜsᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl]
    rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU
    rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]
  tfae_have 2 → 3 := by
    refine fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has ?_, H s a⟩
    exact (hd.symm.mono_right <| @principal_le_nhdsSet _ _ s).eq_bot
  tfae_have 3 → 1 := fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩
  tfae_finish

Equivalent Characterizations of Regular Spaces

Informal description

For a topological space $ X $, the following statements are equivalent: 1. $ X $ is a regular space. 2. For any subset $ s \subseteq X $ and any point $ x \notin \overline{s} $, the neighborhood filter of $ s $ and the neighborhood filter of $ x $ are disjoint. 3. For any point $ x \in X $ and subset $ s \subseteq X $, the neighborhood filter of $ s $ and the neighborhood filter of $ x $ are disjoint if and only if $ x \notin \overline{s} $. 4. For any point $ x \in X $ and any neighborhood $ s $ of $ x $, there exists a closed neighborhood $ t $ of $ x $ such that $ t \subseteq s $. 5. For any point $ x \in X $, the filter generated by the closures of sets in the neighborhood filter of $ x $ is contained in the neighborhood filter of $ x $. 6. For any point $ x \in X $, the filter generated by the closures of sets in the neighborhood filter of $ x $ is equal to the neighborhood filter of $ x $.

RegularSpace.of_lift'_closure_le theorem

(h : ∀ x : X, (𝓝 x).lift' closure ≤ 𝓝 x) : RegularSpace X

Full source

theorem RegularSpace.of_lift'_closure_le (h : ∀ x : X, (𝓝 x).lift' closure ≤ 𝓝 x) :
    RegularSpace X :=
  Iff.mpr ((regularSpace_TFAE X).out 0 4) h

Regularity via Neighborhood Closure Filter Containment

Informal description

A topological space $ X $ is regular if for every point $ x \in X $, the filter generated by the closures of all neighborhoods of $ x $ is contained in the neighborhood filter of $ x $.

RegularSpace.of_lift'_closure theorem

(h : ∀ x : X, (𝓝 x).lift' closure = 𝓝 x) : RegularSpace X

Full source

theorem RegularSpace.of_lift'_closure (h : ∀ x : X, (𝓝 x).lift' closure = 𝓝 x) : RegularSpace X :=
  Iff.mpr ((regularSpace_TFAE X).out 0 5) h

Regular Space Criterion via Closure of Neighborhoods

Informal description

A topological space $X$ is regular if for every point $x \in X$, the filter generated by the closures of neighborhoods of $x$ is equal to the neighborhood filter of $x$.

RegularSpace.of_hasBasis theorem

 {ι : X → Sort*} {p : ∀ a, ι a → Prop} {s : ∀ a, ι a → Set X} (h₁ : ∀ a, (𝓝 a).HasBasis (p a) (s a))
  (h₂ : ∀ a i, p a i → IsClosed (s a i)) : RegularSpace X

Full source

theorem RegularSpace.of_hasBasis {ι : X → Sort*} {p : ∀ a, ι a → Prop} {s : ∀ a, ι a → Set X}
    (h₁ : ∀ a, (𝓝 a).HasBasis (p a) (s a)) (h₂ : ∀ a i, p a i → IsClosed (s a i)) :
    RegularSpace X :=
  .of_lift'_closure fun a => (h₁ a).lift'_closure_eq_self (h₂ a)

Regularity from Closed Neighborhood Basis

Informal description

Let $X$ be a topological space with a basis $\{s(a, i)\}_{i \in \iota(a)}$ for the neighborhood filter of each point $a \in X$, where $\iota(a)$ is an index type and $p(a, i)$ is a predicate on the indices. If for every $a \in X$ and $i \in \iota(a)$, the set $s(a, i)$ is closed whenever $p(a, i)$ holds, then $X$ is a regular space.

RegularSpace.of_exists_mem_nhds_isClosed_subset theorem

(h : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s) : RegularSpace X

Full source

theorem RegularSpace.of_exists_mem_nhds_isClosed_subset
    (h : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s) : RegularSpace X :=
  Iff.mpr ((regularSpace_TFAE X).out 0 3) h

Characterization of Regular Spaces via Closed Neighborhood Bases

Informal description

A topological space $ X $ is regular if for every point $ x \in X $ and every neighborhood $ s $ of $ x $, there exists a closed neighborhood $ t $ of $ x $ such that $ t \subseteq s $.

instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space instance

[WeaklyLocallyCompactSpace X] [R1Space X] : RegularSpace X

Full source

/-- A weakly locally compact R₁ space is regular. -/
instance (priority := 100) [WeaklyLocallyCompactSpace X] [R1Space X] : RegularSpace X :=
  .of_hasBasis isCompact_isClosed_basis_nhds fun _ _ ⟨_, _, h⟩ ↦ h

Weakly Locally Compact Preregular Spaces are Regular

Informal description

Every weakly locally compact preregular (R₁) space is regular. That is, if a topological space $X$ is weakly locally compact (every point has a compact neighborhood) and preregular (any two topologically distinguishable points have disjoint neighborhoods), then $X$ is regular (for any closed set $C$ and point $x \notin C$, there exist disjoint open sets containing $x$ and $C$ respectively).

disjoint_nhdsSet_nhds theorem

: Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s

Full source

theorem disjoint_nhdsSet_nhds : DisjointDisjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s := by
  have h := (regularSpace_TFAE X).out 0 2
  exact h.mp ‹_› _ _

Disjoint Neighborhood Filters and Closure Condition

Informal description

For any subset $s$ of a topological space $X$ and any point $x \in X$, the neighborhood filter of $s$ and the neighborhood filter of $x$ are disjoint if and only if $x$ does not belong to the closure of $s$.

disjoint_nhds_nhdsSet theorem

: Disjoint (𝓝 x) (𝓝ˢ s) ↔ x ∉ closure s

Full source

theorem disjoint_nhds_nhdsSet : DisjointDisjoint (𝓝 x) (𝓝ˢ s) ↔ x ∉ closure s :=
  disjoint_comm.trans disjoint_nhdsSet_nhds

Disjoint Neighborhood Filters and Closure Condition (Symmetric Version)

Informal description

For any point $x$ in a topological space $X$ and any subset $s \subseteq X$, the neighborhood filter of $x$ and the neighborhood filter of $s$ are disjoint if and only if $x$ does not belong to the closure of $s$, i.e., $\text{Disjoint}(\mathcal{N}(x), \mathcal{N}(s)) \leftrightarrow x \notin \overline{s}$.

instR1Space instance

: R1Space X

Full source

/-- A regular space is R₁. -/
instance (priority := 100) : R1Space X where
  specializes_or_disjoint_nhds _ _ := or_iff_not_imp_left.2 fun h ↦ by
    rwa [← nhdsSet_singleton, disjoint_nhdsSet_nhds, ← specializes_iff_mem_closure]

Regular Spaces are Preregular

Informal description

Every regular topological space is preregular (R₁).

exists_mem_nhds_isClosed_subset theorem

{x : X} {s : Set X} (h : s ∈ 𝓝 x) : ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

Full source

theorem exists_mem_nhds_isClosed_subset {x : X} {s : Set X} (h : s ∈ 𝓝 x) :
    ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s := by
  have h' := (regularSpace_TFAE X).out 0 3
  exact h'.mp ‹_› _ _ h

Existence of Closed Neighborhoods Within Any Neighborhood in a Regular Space

Informal description

For any point $x$ in a topological space $X$ and any neighborhood $s$ of $x$, there exists a closed neighborhood $t$ of $x$ such that $t \subseteq s$.

closed_nhds_basis theorem

(x : X) : (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 x ∧ IsClosed s) id

Full source

theorem closed_nhds_basis (x : X) : (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 xs ∈ 𝓝 x ∧ IsClosed s) id :=
  hasBasis_self.2 fun _ => exists_mem_nhds_isClosed_subset

Closed Neighborhoods Form a Basis for the Neighborhood Filter in a Regular Space

Informal description

For any point $x$ in a regular topological space $X$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of closed neighborhoods of $x$. That is, every neighborhood of $x$ contains a closed neighborhood of $x$.

lift'_nhds_closure theorem

(x : X) : (𝓝 x).lift' closure = 𝓝 x

Full source

theorem lift'_nhds_closure (x : X) : (𝓝 x).lift' closure = 𝓝 x :=
  (closed_nhds_basis x).lift'_closure_eq_self fun _ => And.right

Closure of Neighborhoods Generates Original Neighborhood Filter in Regular Spaces

Informal description

For any point $x$ in a regular topological space $X$, the filter generated by taking the closure of every neighborhood of $x$ is equal to the neighborhood filter of $x$ itself. In other words, $\mathcal{N}(x) = \text{lift}'(\text{closure}, \mathcal{N}(x))$.

Filter.HasBasis.nhds_closure theorem

 {ι : Sort*} {x : X} {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) : (𝓝 x).HasBasis p fun i => closure (s i)

Full source

theorem Filter.HasBasis.nhds_closure {ι : Sort*} {x : X} {p : ι → Prop} {s : ι → Set X}
    (h : (𝓝 x).HasBasis p s) : (𝓝 x).HasBasis p fun i => closure (s i) :=
  lift'_nhds_closure x ▸ h.lift'_closure

Closures of a neighborhood basis form a neighborhood basis

Informal description

Let $X$ be a topological space, $x \in X$, and suppose the neighborhood filter $\mathcal{N}(x)$ has a basis $\{s_i\}_{i \in \iota}$ indexed by some type $\iota$ with a predicate $p$. Then the closures $\{\overline{s_i}\}_{i \in \iota}$ also form a basis for $\mathcal{N}(x)$, with the same index type and predicate.

hasBasis_nhds_closure theorem

(x : X) : (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x) closure

Full source

theorem hasBasis_nhds_closure (x : X) : (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x) closure :=
  (𝓝 x).basis_sets.nhds_closure

Neighborhood Filter Basis via Closures

Informal description

For any point $x$ in a topological space $X$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the closures of all neighborhoods of $x$. That is, the collection $\{\overline{s} \mid s \in \mathcal{N}(x)\}$ forms a basis for $\mathcal{N}(x)$.

hasBasis_opens_closure theorem

(x : X) : (𝓝 x).HasBasis (fun s => x ∈ s ∧ IsOpen s) closure

Full source

theorem hasBasis_opens_closure (x : X) : (𝓝 x).HasBasis (fun s => x ∈ sx ∈ s ∧ IsOpen s) closure :=
  (nhds_basis_opens x).nhds_closure

Neighborhood Basis via Closures of Open Sets

Informal description

For any point $x$ in a topological space $X$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the closures of all open sets containing $x$. That is, the collection $\{\overline{U} \mid U \text{ is open and } x \in U\}$ forms a basis for $\mathcal{N}(x)$.

IsCompact.exists_isOpen_closure_subset theorem

{K U : Set X} (hK : IsCompact K) (hU : U ∈ 𝓝ˢ K) : ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U

Full source

theorem IsCompact.exists_isOpen_closure_subset {K U : Set X} (hK : IsCompact K) (hU : U ∈ 𝓝ˢ K) :
    ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U := by
  have hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ) := by
    simpa [hK.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
      ← subset_interior_iff_mem_nhdsSet] using hU
  rcases ((hasBasis_nhdsSet _).disjoint_iff (hasBasis_nhdsSet _)).1 hd
    with ⟨V, ⟨hVo, hKV⟩, W, ⟨hW, hUW⟩, hVW⟩
  refine ⟨V, hVo, hKV, Subset.trans ?_ (compl_subset_comm.1 hUW)⟩
  exact closure_minimal hVW.subset_compl_right hW.isClosed_compl

Existence of Open Neighborhood with Closure Contained in Given Neighborhood for Compact Sets

Informal description

Let $ X $ be a topological space, $ K \subseteq X $ a compact subset, and $ U $ a neighborhood of $ K $. Then there exists an open set $ V $ such that $ K \subseteq V $ and the closure of $ V $ is contained in $ U $.

IsCompact.lift'_closure_nhdsSet theorem

{K : Set X} (hK : IsCompact K) : (𝓝ˢ K).lift' closure = 𝓝ˢ K

Full source

theorem IsCompact.lift'_closure_nhdsSet {K : Set X} (hK : IsCompact K) :
    (𝓝ˢ K).lift' closure = 𝓝ˢ K := by
  refine le_antisymm (fun U hU ↦ ?_) (le_lift'_closure _)
  rcases hK.exists_isOpen_closure_subset hU with ⟨V, hVo, hKV, hVU⟩
  exact mem_of_superset (mem_lift' <| hVo.mem_nhdsSet.2 hKV) hVU

Closure of Neighborhoods of Compact Sets Generates Neighborhood Filter

Informal description

For any compact subset $K$ of a topological space $X$, the filter generated by the closures of all neighborhoods of $K$ is equal to the neighborhood filter of $K$. In other words, $\text{lift}'(\text{closure})(\mathcal{N}(K)) = \mathcal{N}(K)$, where $\mathcal{N}(K)$ denotes the neighborhood filter of $K$.

TopologicalSpace.IsTopologicalBasis.nhds_basis_closure theorem

 {B : Set (Set X)} (hB : IsTopologicalBasis B) (x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∈ s ∧ s ∈ B) closure

Full source

theorem TopologicalSpace.IsTopologicalBasis.nhds_basis_closure {B : Set (Set X)}
    (hB : IsTopologicalBasis B) (x : X) :
    (𝓝 x).HasBasis (fun s : Set X => x ∈ sx ∈ s ∧ s ∈ B) closure := by
  simpa only [and_comm] using hB.nhds_hasBasis.nhds_closure

Neighborhood Basis via Closures of Basis Sets

Informal description

Let $X$ be a topological space with a topological basis $B$. For any point $x \in X$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the closures of sets in $B$ that contain $x$. In other words, for any $s \in B$ with $x \in s$, the closure $\overline{s}$ forms a neighborhood basis at $x$.

TopologicalSpace.IsTopologicalBasis.exists_closure_subset theorem

 {B : Set (Set X)} (hB : IsTopologicalBasis B) {x : X} {s : Set X} (h : s ∈ 𝓝 x) : ∃ t ∈ B, x ∈ t ∧ closure t ⊆ s

Full source

theorem TopologicalSpace.IsTopologicalBasis.exists_closure_subset {B : Set (Set X)}
    (hB : IsTopologicalBasis B) {x : X} {s : Set X} (h : s ∈ 𝓝 x) :
    ∃ t ∈ B, x ∈ t ∧ closure t ⊆ s := by
  simpa only [exists_prop, and_assoc] using hB.nhds_hasBasis.nhds_closure.mem_iff.mp h

Existence of Basis Element with Closure in Neighborhood

Informal description

Let $X$ be a topological space with a basis $B$ for its topology. For any point $x \in X$ and any neighborhood $s$ of $x$, there exists a basis element $t \in B$ such that $x \in t$ and the closure of $t$ is contained in $s$.

Topology.IsInducing.regularSpace theorem

[TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) : RegularSpace Y

Full source

protected theorem Topology.IsInducing.regularSpace [TopologicalSpace Y] {f : Y → X}
    (hf : IsInducing f) : RegularSpace Y :=
  .of_hasBasis
    (fun b => by rw [hf.nhds_eq_comap b]; exact (closed_nhds_basis _).comap _)
    fun b s hs => by exact hs.2.preimage hf.continuous

Regularity is Preserved under Induced Topology

Informal description

Let $Y$ be a topological space and $f : Y \to X$ be a continuous map that induces the topology on $Y$ (i.e., the topology on $Y$ is the coarsest topology making $f$ continuous). If $X$ is a regular space, then $Y$ is also a regular space.

regularSpace_induced theorem

(f : Y → X) : @RegularSpace Y (induced f ‹_›)

Full source

theorem regularSpace_induced (f : Y → X) : @RegularSpace Y (induced f ‹_›) :=
  letI := induced f ‹_›
  (IsInducing.induced f).regularSpace

Regularity is Preserved under Induced Topology

Informal description

Let $X$ be a topological space and $Y$ be a set. Given a function $f : Y \to X$, the induced topology on $Y$ (i.e., the coarsest topology making $f$ continuous) is regular if $X$ is regular.

regularSpace_sInf theorem

{X} {T : Set (TopologicalSpace X)} (h : ∀ t ∈ T, @RegularSpace X t) : @RegularSpace X (sInf T)

Full source

theorem regularSpace_sInf {X} {T : Set (TopologicalSpace X)} (h : ∀ t ∈ T, @RegularSpace X t) :
    @RegularSpace X (sInf T) := by
  let _ := sInf T
  have : ∀ a, (𝓝 a).HasBasis
      (fun If : Σ I : Set T, I → Set X =>
        If.1.Finite ∧ ∀ i : If.1, If.2 i ∈ @nhds X i a ∧ @IsClosed X i (If.2 i))
      fun If => ⋂ i : If.1, If.snd i := fun a ↦ by
    rw [nhds_sInf, ← iInf_subtype'']
    exact hasBasis_iInf fun t : T => @closed_nhds_basis X t (h t t.2) a
  refine .of_hasBasis this fun a If hIf => isClosed_iInter fun i => ?_
  exact (hIf.2 i).2.mono (sInf_le (i : T).2)

Infimum of Regular Topologies is Regular

Informal description

Let $X$ be a set equipped with a collection of topological spaces $\{t\}_{t \in T}$ indexed by a set $T$. If each topological space $t \in T$ is regular, then the infimum topology (the intersection of all topologies in $T$) on $X$ is also regular.

regularSpace_iInf theorem

{ι X} {t : ι → TopologicalSpace X} (h : ∀ i, @RegularSpace X (t i)) : @RegularSpace X (iInf t)

Full source

theorem regularSpace_iInf {ι X} {t : ι → TopologicalSpace X} (h : ∀ i, @RegularSpace X (t i)) :
    @RegularSpace X (iInf t) :=
  regularSpace_sInf <| forall_mem_range.mpr h

Infimum of Regular Topologies is Regular

Informal description

Let $X$ be a set and $\{t_i\}_{i \in \iota}$ be a family of topological spaces on $X$. If each topological space $t_i$ is regular, then the infimum topology $\bigsqcap_{i \in \iota} t_i$ on $X$ is also regular.

RegularSpace.inf theorem

 {X} {t₁ t₂ : TopologicalSpace X} (h₁ : @RegularSpace X t₁) (h₂ : @RegularSpace X t₂) : @RegularSpace X (t₁ ⊓ t₂)

Full source

theorem RegularSpace.inf {X} {t₁ t₂ : TopologicalSpace X} (h₁ : @RegularSpace X t₁)
    (h₂ : @RegularSpace X t₂) : @RegularSpace X (t₁ ⊓ t₂) := by
  rw [inf_eq_iInf]
  exact regularSpace_iInf (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Infimum of Two Regular Topologies is Regular

Informal description

Let $X$ be a set equipped with two topological spaces $t_1$ and $t_2$. If both $t_1$ and $t_2$ are regular, then the infimum topology $t_1 \sqcap t_2$ on $X$ is also regular.

instRegularSpaceSubtype instance

{p : X → Prop} : RegularSpace (Subtype p)

Full source

instance {p : X → Prop} : RegularSpace (Subtype p) :=
  IsEmbedding.subtypeVal.isInducing.regularSpace

Subspaces of Regular Spaces are Regular

Informal description

For any topological space $X$ and any subset defined by a predicate $p : X \to \mathrm{Prop}$, the subspace topology on $\{x \in X \mid p(x)\}$ is regular if $X$ is regular.

instRegularSpaceProd instance

[TopologicalSpace Y] [RegularSpace Y] : RegularSpace (X × Y)

Full source

instance [TopologicalSpace Y] [RegularSpace Y] : RegularSpace (X × Y) :=
  (regularSpace_induced (@Prod.fst X Y)).inf (regularSpace_induced (@Prod.snd X Y))

Product of Regular Spaces is Regular

Informal description

For any topological spaces $X$ and $Y$, if $Y$ is regular, then the product space $X \times Y$ with the product topology is also regular.

instRegularSpaceForall instance

{ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, RegularSpace (X i)] : RegularSpace (∀ i, X i)

Full source

instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, RegularSpace (X i)] :
    RegularSpace (∀ i, X i) :=
  regularSpace_iInf fun _ => regularSpace_induced _

Product of Regular Spaces is Regular

Informal description

For any family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is a regular space, the product space $\prod_{i \in \iota} X_i$ equipped with the product topology is also a regular space.

SeparatedNhds.of_isCompact_isClosed theorem

{s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) : SeparatedNhds s t

Full source

/-- In a regular space, if a compact set and a closed set are disjoint, then they have disjoint
neighborhoods. -/
lemma SeparatedNhds.of_isCompact_isClosed {s t : Set X}
    (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) : SeparatedNhds s t := by
  simpa only [separatedNhds_iff_disjoint, hs.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
    ht.closure_eq, disjoint_left] using hst

Disjoint Compact and Closed Sets Have Disjoint Neighborhoods in Regular Spaces

Informal description

Let $ X $ be a topological space, and let $ s, t \subseteq X $ be disjoint subsets where $ s $ is compact and $ t $ is closed. Then there exist disjoint open sets $ U $ and $ V $ such that $ s \subseteq U $ and $ t \subseteq V $.

IsClosed.HasSeparatingCover theorem

 {s t : Set X} [LindelofSpace X] [RegularSpace X] (s_cl : IsClosed s) (t_cl : IsClosed t) (st_dis : Disjoint s t) :
  HasSeparatingCover s t

Full source

/-- This technique to witness `HasSeparatingCover` in regular Lindelöf topological spaces
will be used to prove regular Lindelöf spaces are normal. -/
lemma IsClosed.HasSeparatingCover {s t : Set X} [LindelofSpace X] [RegularSpace X]
    (s_cl : IsClosed s) (t_cl : IsClosed t) (st_dis : Disjoint s t) : HasSeparatingCover s t := by
  -- `IsLindelof.indexed_countable_subcover` requires the space be Nonempty
  rcases isEmpty_or_nonempty X with empty_X | nonempty_X
  · rw [subset_eq_empty (t := s) (fun ⦃_⦄ _ ↦ trivial) (univ_eq_empty_iff.mpr empty_X)]
    exact hasSeparatingCovers_iff_separatedNhds.mpr (SeparatedNhds.empty_left t) |>.1
  -- This is almost `HasSeparatingCover`, but is not countable. We define for all `a : X` for use
  -- with `IsLindelof.indexed_countable_subcover` momentarily.
  have (a : X) : ∃ n : Set X, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n) := by
    wlog ains : a ∈ s
    · exact ⟨∅, isOpen_empty, SeparatedNhds.empty_left t |>.disjoint_closure_left, fun a ↦ ains a⟩
    obtain ⟨n, nna, ncl, nsubkc⟩ := ((regularSpace_TFAE X).out 0 3 :).mp ‹RegularSpace X› a tᶜ <|
      t_cl.compl_mem_nhds (disjoint_left.mp st_dis ains)
    exact
      ⟨interior n,
       isOpen_interior,
       disjoint_left.mpr fun ⦃_⦄ ain ↦
         nsubkc <| (IsClosed.closure_subset_iff ncl).mpr interior_subset ain,
       fun _ ↦ mem_interior_iff_mem_nhds.mpr nna⟩
  -- By Lindelöf, we may obtain a countable subcover witnessing `HasSeparatingCover`
  choose u u_open u_dis u_nhd using this
  obtain ⟨f, f_cov⟩ := s_cl.isLindelof.indexed_countable_subcover
    u u_open (fun a ainh ↦ mem_iUnion.mpr ⟨a, u_nhd a ainh⟩)
  exact ⟨u ∘ f, f_cov, fun n ↦ ⟨u_open (f n), u_dis (f n)⟩⟩

Existence of Separating Open Cover for Disjoint Closed Sets in Lindelöf Regular Spaces

Informal description

Let $ X $ be a Lindelöf regular topological space, and let $ s, t \subseteq X $ be disjoint closed sets. Then there exists a separating open cover for $ s $ and $ t $, meaning there exist open sets $ U $ and $ V $ such that $ s \subseteq U $, $ t \subseteq V $, and $ U \cap V = \emptyset $.

exists_compact_closed_between theorem

 [LocallyCompactSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K ⊆ U) :
  ∃ L, IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ L ⊆ U

Full source

/-- In a (possibly non-Hausdorff) locally compact regular space, for every containment `K ⊆ U` of
  a compact set `K` in an open set `U`, there is a compact closed neighborhood `L`
  such that `K ⊆ L ⊆ U`: equivalently, there is a compact closed set `L` such
  that `K ⊆ interior L` and `L ⊆ U`. -/
theorem exists_compact_closed_between [LocallyCompactSpace X] [RegularSpace X]
    {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K ⊆ U) :
    ∃ L, IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ L ⊆ U :=
  let ⟨L, L_comp, KL, LU⟩ := exists_compact_between hK hU h_KU
  ⟨closure L, L_comp.closure, isClosed_closure, KL.trans <| interior_mono subset_closure,
    L_comp.closure_subset_of_isOpen hU LU⟩

Existence of Compact Closed Intermediate Set in Locally Compact Regular Spaces

Informal description

Let $X$ be a locally compact regular space, $K \subseteq X$ a compact subset, and $U \subseteq X$ an open set containing $K$. Then there exists a compact closed set $L \subseteq X$ such that $K$ is contained in the interior of $L$ and $L \subseteq U$.

exists_open_between_and_isCompact_closure theorem

 [LocallyCompactSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
  ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)

Full source

/-- In a locally compact regular space, given a compact set `K` inside an open set `U`, we can find
an open set `V` between these sets with compact closure: `K ⊆ V` and the closure of `V` is
inside `U`. -/
theorem exists_open_between_and_isCompact_closure [LocallyCompactSpace X] [RegularSpace X]
    {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
    ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V) := by
  rcases exists_compact_closed_between hK hU hKU with ⟨L, L_compact, L_closed, KL, LU⟩
  have A : closureclosure (interior L) ⊆ L := by
    apply (closure_mono interior_subset).trans (le_of_eq L_closed.closure_eq)
  refine ⟨interior L, isOpen_interior, KL, A.trans LU, ?_⟩
  exact L_compact.closure_of_subset interior_subset

Existence of Open Set with Compact Closure Between Compact Set and Open Superset in Locally Compact Regular Spaces

Informal description

Let $X$ be a locally compact regular space, $K \subseteq X$ a compact subset, and $U \subseteq X$ an open set containing $K$. Then there exists an open set $V$ such that: 1. $K \subseteq V$, 2. The closure of $V$ is contained in $U$, 3. The closure of $V$ is compact.

T25Space structure

(X : Type u) [TopologicalSpace X]

Full source

/-- A T₂.₅ space, also known as a Urysohn space, is a topological space
  where for every pair `x ≠ y`, there are two open sets, with the intersection of closures
  empty, one containing `x` and the other `y` . -/
class T25Space (X : Type u) [TopologicalSpace X] : Prop where
  /-- Given two distinct points in a T₂.₅ space, their filters of closed neighborhoods are
  disjoint. -/
  t2_5 : ∀ ⦃x y : X⦄, x ≠ y → Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure)

T₂.₅ Space (Urysohn Space)

Informal description

A T₂.₅ space (also known as a Urysohn space) is a topological space $X$ where for any two distinct points $x \neq y$, there exist open neighborhoods $U$ of $x$ and $V$ of $y$ such that the closures of $U$ and $V$ are disjoint.

disjoint_lift'_closure_nhds theorem

[T25Space X] {x y : X} : Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure) ↔ x ≠ y

Full source

@[simp]
theorem disjoint_lift'_closure_nhds [T25Space X] {x y : X} :
    DisjointDisjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure) ↔ x ≠ y :=
  ⟨fun h hxy => by simp [hxy, nhds_neBot.ne] at h, fun h => T25Space.t2_5 h⟩

Neighborhood Closure Disjointness Characterization in T₂.₅ Spaces

Informal description

In a T₂.₅ space $X$, for any two points $x$ and $y$, the closures of their neighborhoods are disjoint if and only if $x \neq y$. That is, $\text{Disjoint}(\overline{\mathcal{N}(x)}, \overline{\mathcal{N}(y)}) \leftrightarrow x \neq y$, where $\mathcal{N}(x)$ denotes the neighborhood filter at $x$ and $\overline{A}$ denotes the closure of a set $A$.

T25Space.t2Space instance

[T25Space X] : T2Space X

Full source

instance (priority := 100) T25Space.t2Space [T25Space X] : T2Space X :=
  t2Space_iff_disjoint_nhds.2 fun _ _ hne =>
    (disjoint_lift'_closure_nhds.2 hne).mono (le_lift'_closure _) (le_lift'_closure _)

T₂.₅ Spaces are Hausdorff

Informal description

Every T₂.₅ space is a Hausdorff (T₂) space.

exists_nhds_disjoint_closure theorem

[T25Space X] {x y : X} (h : x ≠ y) : ∃ s ∈ 𝓝 x, ∃ t ∈ 𝓝 y, Disjoint (closure s) (closure t)

Full source

theorem exists_nhds_disjoint_closure [T25Space X] {x y : X} (h : x ≠ y) :
    ∃ s ∈ 𝓝 x, ∃ t ∈ 𝓝 y, Disjoint (closure s) (closure t) :=
  ((𝓝 x).basis_sets.lift'_closure.disjoint_iff (𝓝 y).basis_sets.lift'_closure).1 <|
    disjoint_lift'_closure_nhds.2 h

Existence of Disjoint Closed Neighborhoods for Distinct Points in T₂.₅ Spaces

Informal description

In a T₂.₅ space $X$, for any two distinct points $x$ and $y$, there exist neighborhoods $s$ of $x$ and $t$ of $y$ such that the closures of $s$ and $t$ are disjoint. That is, there exist $s \in \mathcal{N}(x)$ and $t \in \mathcal{N}(y)$ with $\overline{s} \cap \overline{t} = \varnothing$.

exists_open_nhds_disjoint_closure theorem

 [T25Space X] {x y : X} (h : x ≠ y) :
  ∃ u : Set X, x ∈ u ∧ IsOpen u ∧ ∃ v : Set X, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v)

Full source

theorem exists_open_nhds_disjoint_closure [T25Space X] {x y : X} (h : x ≠ y) :
    ∃ u : Set X,
      x ∈ u ∧ IsOpen u ∧ ∃ v : Set X, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v) := by
  simpa only [exists_prop, and_assoc] using
    ((nhds_basis_opens x).lift'_closure.disjoint_iff (nhds_basis_opens y).lift'_closure).1
      (disjoint_lift'_closure_nhds.2 h)

Existence of Disjoint Closed Neighborhoods in T₂.₅ Spaces

Informal description

In a T₂.₅ space $X$, for any two distinct points $x$ and $y$, there exist open neighborhoods $u$ of $x$ and $v$ of $y$ such that the closures of $u$ and $v$ are disjoint. That is, there exist open sets $u$ and $v$ with $x \in u$, $y \in v$, and $\overline{u} \cap \overline{v} = \varnothing$.

T25Space.of_injective_continuous theorem

[TopologicalSpace Y] [T25Space Y] {f : X → Y} (hinj : Injective f) (hcont : Continuous f) : T25Space X

Full source

theorem T25Space.of_injective_continuous [TopologicalSpace Y] [T25Space Y] {f : X → Y}
    (hinj : Injective f) (hcont : Continuous f) : T25Space X where
  t2_5 x y hne := (tendsto_lift'_closure_nhds hcont x).disjoint (t2_5 <| hinj.ne hne)
    (tendsto_lift'_closure_nhds hcont y)

Injective Continuous Maps Preserve T₂.₅ Property

Informal description

Let $X$ and $Y$ be topological spaces, with $Y$ being a T₂.₅ (Urysohn) space. If $f: X \to Y$ is an injective continuous function, then $X$ is also a T₂.₅ space.

Topology.IsEmbedding.t25Space theorem

[TopologicalSpace Y] [T25Space Y] {f : X → Y} (hf : IsEmbedding f) : T25Space X

Full source

theorem Topology.IsEmbedding.t25Space [TopologicalSpace Y] [T25Space Y] {f : X → Y}
    (hf : IsEmbedding f) : T25Space X :=
  .of_injective_continuous hf.injective hf.continuous

Embeddings Preserve T₂.₅ Property

Informal description

Let $X$ and $Y$ be topological spaces, with $Y$ being a T₂.₅ (Urysohn) space. If $f: X \to Y$ is an embedding (i.e., a homeomorphism onto its image), then $X$ is also a T₂.₅ space.

Homeomorph.t25Space theorem

[TopologicalSpace Y] [T25Space X] (h : X ≃ₜ Y) : T25Space Y

Full source

protected theorem Homeomorph.t25Space [TopologicalSpace Y] [T25Space X] (h : X ≃ₜ Y) : T25Space Y :=
  h.symm.isEmbedding.t25Space

Homeomorphisms Preserve T₂.₅ Property

Informal description

Let $X$ and $Y$ be topological spaces, with $X$ being a T₂.₅ (Urysohn) space. If $h: X \to Y$ is a homeomorphism, then $Y$ is also a T₂.₅ space.

Subtype.instT25Space instance

[T25Space X] {p : X → Prop} : T25Space { x // p x }

Full source

instance Subtype.instT25Space [T25Space X] {p : X → Prop} : T25Space {x // p x} :=
  IsEmbedding.subtypeVal.t25Space

Subtypes of T₂.₅ Spaces are T₂.₅

Informal description

For any topological space $X$ that is a T₂.₅ space and any predicate $p$ on $X$, the subtype $\{x \in X \mid p(x)\}$ is also a T₂.₅ space.

T3Space structure

(X : Type u) [TopologicalSpace X] : Prop extends T0Space X, RegularSpace X

Full source

/-- A T₃ space is a T₀ space which is a regular space. Any T₃ space is a T₁ space, a T₂ space, and
a T₂.₅ space. -/
class T3Space (X : Type u) [TopologicalSpace X] : Prop extends T0Space X, RegularSpace X

T₃ space (regular T₀ space)

Informal description

A T₃ space is a topological space that is both a T₀ space (Kolmogorov) and a regular space. In a T₃ space, for any point $ x $ and closed set $ C $ not containing $ x $, there exist disjoint open sets $ U $ and $ V $ such that $ x \in U $ and $ C \subseteq V $.

instT3Space instance

[T0Space X] [RegularSpace X] : T3Space X

Full source

instance (priority := 90) instT3Space [T0Space X] [RegularSpace X] : T3Space X := ⟨⟩

T₀ and Regular Implies T₃

Informal description

Every topological space $X$ that is both a T₀ space and a regular space is a T₃ space.

RegularSpace.t3Space_iff_t0Space theorem

[RegularSpace X] : T3Space X ↔ T0Space X

Full source

theorem RegularSpace.t3Space_iff_t0Space [RegularSpace X] : T3SpaceT3Space X ↔ T0Space X := by
  constructor <;> intro <;> infer_instance

Characterization of T₃ Spaces via T₀ and Regularity

Informal description

For a topological space $ X $ that is regular, $ X $ is a T₃ space if and only if it is a T₀ space.

T3Space.t25Space instance

[T3Space X] : T25Space X

Full source

instance (priority := 100) T3Space.t25Space [T3Space X] : T25Space X := by
  refine ⟨fun x y hne => ?_⟩
  rw [lift'_nhds_closure, lift'_nhds_closure]
  have : x ∉ closure {y}x ∉ closure {y} ∨ y ∉ closure {x} :=
    (t0Space_iff_or_not_mem_closure X).mp inferInstance hne
  simp only [← disjoint_nhds_nhdsSet, nhdsSet_singleton] at this
  exact this.elim id fun h => h.symm

T₃ Spaces are T₂.₅ Spaces

Informal description

Every T₃ space is also a T₂.₅ space.

Topology.IsEmbedding.t3Space theorem

[TopologicalSpace Y] [T3Space Y] {f : X → Y} (hf : IsEmbedding f) : T3Space X

Full source

protected theorem Topology.IsEmbedding.t3Space [TopologicalSpace Y] [T3Space Y] {f : X → Y}
    (hf : IsEmbedding f) : T3Space X :=
  { toT0Space := hf.t0Space
    toRegularSpace := hf.isInducing.regularSpace }

T₃ Property via Embedding

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be an embedding (a continuous injective map that is a homeomorphism onto its image). If $Y$ is a T₃ space, then $X$ is also a T₃ space.

Homeomorph.t3Space theorem

[TopologicalSpace Y] [T3Space X] (h : X ≃ₜ Y) : T3Space Y

Full source

protected theorem Homeomorph.t3Space [TopologicalSpace Y] [T3Space X] (h : X ≃ₜ Y) : T3Space Y :=
  h.symm.isEmbedding.t3Space

T₃ Property Preserved Under Homeomorphism

Informal description

Let $X$ and $Y$ be topological spaces, and let $h: X \simeq Y$ be a homeomorphism between them. If $X$ is a T₃ space, then $Y$ is also a T₃ space.

Subtype.t3Space instance

[T3Space X] {p : X → Prop} : T3Space (Subtype p)

Full source

instance Subtype.t3Space [T3Space X] {p : X → Prop} : T3Space (Subtype p) :=
  IsEmbedding.subtypeVal.t3Space

T₃ Property of Subspaces

Informal description

For any topological space $X$ that is a T₃ space and any predicate $p$ on $X$, the subspace $\{x \in X \mid p(x)\}$ is also a T₃ space.

ULift.instT3Space instance

[T3Space X] : T3Space (ULift X)

Full source

instance ULift.instT3Space [T3Space X] : T3Space (ULift X) :=
  IsEmbedding.uliftDown.t3Space

T₃ Property Preserved Under ULift

Informal description

For any T₃ space $X$, the lifted space $\text{ULift}\, X$ is also a T₃ space.

instT3SpaceProd instance

[TopologicalSpace Y] [T3Space X] [T3Space Y] : T3Space (X × Y)

Full source

instance [TopologicalSpace Y] [T3Space X] [T3Space Y] : T3Space (X × Y) := ⟨⟩

Product of T₃ Spaces is T₃

Informal description

For any topological spaces $X$ and $Y$ that are T₃ spaces, their product space $X \times Y$ with the product topology is also a T₃ space.

instT3SpaceForall instance

{ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T3Space (X i)] : T3Space (∀ i, X i)

Full source

instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T3Space (X i)] :
    T3Space (∀ i, X i) := ⟨⟩

Product of T₃ Spaces is T₃

Informal description

For any family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is a T₃ space, the product space $\prod_{i \in \iota} X_i$ equipped with the product topology is also a T₃ space.

disjoint_nested_nhds theorem

 [T3Space X] {x y : X} (h : x ≠ y) :
  ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Full source

/-- Given two points `x ≠ y`, we can find neighbourhoods `x ∈ V₁ ⊆ U₁` and `y ∈ V₂ ⊆ U₂`,
with the `Vₖ` closed and the `Uₖ` open, such that the `Uₖ` are disjoint. -/
theorem disjoint_nested_nhds [T3Space X] {x y : X} (h : x ≠ y) :
    ∃ U₁ ∈ 𝓝 x, ∃ V₁ ∈ 𝓝 x, ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y,
      IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂ := by
  rcases t2_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩
  rcases exists_mem_nhds_isClosed_subset (U₁_op.mem_nhds x_in) with ⟨V₁, V₁_in, V₁_closed, h₁⟩
  rcases exists_mem_nhds_isClosed_subset (U₂_op.mem_nhds y_in) with ⟨V₂, V₂_in, V₂_closed, h₂⟩
  exact ⟨U₁, mem_of_superset V₁_in h₁, V₁, V₁_in, U₂, mem_of_superset V₂_in h₂, V₂, V₂_in,
    V₁_closed, V₂_closed, U₁_op, U₂_op, h₁, h₂, H⟩

Existence of Disjoint Nested Neighborhoods in T₃ Spaces

Informal description

Let $ X $ be a T₃ space. For any two distinct points $ x, y \in X $, there exist neighborhoods $ U_1 $ and $ U_2 $ of $ x $ and $ y $ respectively, and closed neighborhoods $ V_1 $ and $ V_2 $ of $ x $ and $ y $ respectively, such that: - $ V_1 \subseteq U_1 $ and $ V_2 \subseteq U_2 $, - $ U_1 $ and $ U_2 $ are open, - $ V_1 $ and $ V_2 $ are closed, - $ U_1 $ and $ U_2 $ are disjoint.

instT3SpaceSeparationQuotientOfRegularSpace instance

[RegularSpace X] : T3Space (SeparationQuotient X)

Full source

/-- The `SeparationQuotient` of a regular space is a T₃ space. -/
instance [RegularSpace X] : T3Space (SeparationQuotient X) where
  regular {s a} hs ha := by
    rcases surjective_mk a with ⟨a, rfl⟩
    rw [← disjoint_comap_iff surjective_mk, comap_mk_nhds_mk, comap_mk_nhdsSet]
    exact RegularSpace.regular (hs.preimage continuous_mk) ha

Separation Quotient of a Regular Space is T₃

Informal description

The separation quotient of a regular topological space $X$ is a T₃ space.

NormalSpace structure

(X : Type u) [TopologicalSpace X]

Full source

/-- A topological space is said to be a *normal space* if any two disjoint closed sets
have disjoint open neighborhoods. -/
class NormalSpace (X : Type u) [TopologicalSpace X] : Prop where
  /-- Two disjoint sets in a normal space admit disjoint neighbourhoods. -/
  normal : ∀ s t : Set X, IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t

Normal space

Informal description

A topological space $ X $ is called a *normal space* if for any two disjoint closed subsets $ s $ and $ t $ of $ X $, there exist disjoint open subsets $ U $ and $ V $ of $ X $ such that $ s \subseteq U $ and $ t \subseteq V $.

normal_separation theorem

[NormalSpace X] {s t : Set X} (H1 : IsClosed s) (H2 : IsClosed t) (H3 : Disjoint s t) : SeparatedNhds s t

Full source

theorem normal_separation [NormalSpace X] {s t : Set X} (H1 : IsClosed s) (H2 : IsClosed t)
    (H3 : Disjoint s t) : SeparatedNhds s t :=
  NormalSpace.normal s t H1 H2 H3

Disjoint Closed Sets in Normal Spaces Have Disjoint Open Neighborhoods

Informal description

Let $ X $ be a normal topological space, and let $ s $ and $ t $ be two disjoint closed subsets of $ X $. Then there exist disjoint open neighborhoods $ U $ and $ V $ of $ s $ and $ t $ respectively, i.e., $ s \subseteq U $, $ t \subseteq V $, and $ U \cap V = \emptyset $.

disjoint_nhdsSet_nhdsSet theorem

[NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : Disjoint (𝓝ˢ s) (𝓝ˢ t)

Full source

theorem disjoint_nhdsSet_nhdsSet [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t)
    (hd : Disjoint s t) : Disjoint (𝓝ˢ s) (𝓝ˢ t) :=
  (normal_separation hs ht hd).disjoint_nhdsSet

Disjoint Neighborhood Filters for Disjoint Closed Sets in Normal Spaces

Informal description

Let $ X $ be a normal topological space, and let $ s $ and $ t $ be two disjoint closed subsets of $ X $. Then the neighborhood filters $ \mathcal{N}(s) $ and $ \mathcal{N}(t) $ of $ s $ and $ t $ respectively are disjoint, meaning there exist disjoint open neighborhoods $ U \in \mathcal{N}(s) $ and $ V \in \mathcal{N}(t) $.

normal_exists_closure_subset theorem

 [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsOpen t) (hst : s ⊆ t) : ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t

Full source

theorem normal_exists_closure_subset [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsOpen t)
    (hst : s ⊆ t) : ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t := by
  have : Disjoint s tᶜ := Set.disjoint_left.mpr fun x hxs hxt => hxt (hst hxs)
  rcases normal_separation hs (isClosed_compl_iff.2 ht) this with
    ⟨s', t', hs', ht', hss', htt', hs't'⟩
  refine ⟨s', hs', hss', Subset.trans (closure_minimal ?_ (isClosed_compl_iff.2 ht'))
    (compl_subset_comm.1 htt')⟩
  exact fun x hxs hxt => hs't'.le_bot ⟨hxs, hxt⟩

Existence of Open Neighborhood with Closure Contained in Larger Open Set in Normal Spaces

Informal description

Let $X$ be a normal topological space, $s$ a closed subset of $X$, and $t$ an open subset of $X$ such that $s \subseteq t$. Then there exists an open set $u$ such that $s \subseteq u$ and the closure of $u$ is contained in $t$.

Topology.IsClosedEmbedding.normalSpace theorem

[TopologicalSpace Y] [NormalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : NormalSpace X

Full source

/-- If the codomain of a closed embedding is a normal space, then so is the domain. -/
protected theorem Topology.IsClosedEmbedding.normalSpace [TopologicalSpace Y] [NormalSpace Y]
    {f : X → Y} (hf : IsClosedEmbedding f) : NormalSpace X where
  normal s t hs ht hst := by
    have H : SeparatedNhds (f '' s) (f '' t) :=
      NormalSpace.normal (f '' s) (f '' t) (hf.isClosedMap s hs) (hf.isClosedMap t ht)
        (disjoint_image_of_injective hf.injective hst)
    exact (H.preimage hf.continuous).mono (subset_preimage_image _ _) (subset_preimage_image _ _)

Normality is Preserved Under Closed Embeddings

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be a closed embedding. If $Y$ is a normal space, then $X$ is also a normal space.

Homeomorph.normalSpace theorem

[TopologicalSpace Y] [NormalSpace X] (h : X ≃ₜ Y) : NormalSpace Y

Full source

protected theorem Homeomorph.normalSpace [TopologicalSpace Y] [NormalSpace X] (h : X ≃ₜ Y) :
    NormalSpace Y :=
  h.symm.isClosedEmbedding.normalSpace

Normality is Preserved Under Homeomorphism

Informal description

Let $X$ and $Y$ be topological spaces, and let $h : X \simeq Y$ be a homeomorphism. If $X$ is a normal space, then $Y$ is also a normal space.

NormalSpace.of_compactSpace_r1Space instance

[CompactSpace X] [R1Space X] : NormalSpace X

Full source

instance (priority := 100) NormalSpace.of_compactSpace_r1Space [CompactSpace X] [R1Space X] :
    NormalSpace X where
  normal _s _t hs ht := .of_isCompact_isCompact_isClosed hs.isCompact ht.isCompact ht

Compact Preregular Spaces are Normal

Informal description

Every compact preregular (R₁) topological space $X$ is normal. That is, for any topological space $X$ that is both compact and preregular, given any two disjoint closed sets $C$ and $D$ in $X$, there exist disjoint open sets $U$ and $V$ containing $C$ and $D$ respectively.

NormalSpace.of_regularSpace_lindelofSpace instance

[RegularSpace X] [LindelofSpace X] : NormalSpace X

Full source

/-- A regular topological space with a Lindelöf topology is a normal space. A consequence of e.g.
Corollaries 20.8 and 20.10 of [Willard's *General Topology*][zbMATH02107988] (without the
assumption of Hausdorff). -/
instance (priority := 100) NormalSpace.of_regularSpace_lindelofSpace
    [RegularSpace X] [LindelofSpace X] : NormalSpace X where
  normal _ _ hcl kcl hkdis :=
    hasSeparatingCovers_iff_separatedNhds.mp
    ⟨hcl.HasSeparatingCover kcl hkdis, kcl.HasSeparatingCover hcl (Disjoint.symm hkdis)⟩

Regular Lindelöf Spaces are Normal

Informal description

Every regular Lindelöf space is normal. That is, for any topological space $X$ that is both regular and Lindelöf, given any two disjoint closed sets $C$ and $D$ in $X$, there exist disjoint open sets $U$ and $V$ containing $C$ and $D$ respectively.

NormalSpace.of_regularSpace_secondCountableTopology instance

[RegularSpace X] [SecondCountableTopology X] : NormalSpace X

Full source

instance (priority := 100) NormalSpace.of_regularSpace_secondCountableTopology
    [RegularSpace X] [SecondCountableTopology X] : NormalSpace X :=
  of_regularSpace_lindelofSpace

Regular Second-Countable Spaces are Normal

Informal description

Every regular second-countable topological space $X$ is normal. That is, for any topological space $X$ that is both regular and second-countable, given any two disjoint closed sets $C$ and $D$ in $X$, there exist disjoint open sets $U$ and $V$ containing $C$ and $D$ respectively.

T4Space structure

(X : Type u) [TopologicalSpace X] : Prop extends T1Space X, NormalSpace X

Full source

/-- A T₄ space is a normal T₁ space. -/
class T4Space (X : Type u) [TopologicalSpace X] : Prop extends T1Space X, NormalSpace X

T₄ Space

Informal description

A T₄ space is a topological space $ X $ that satisfies both the T₁ separation axiom and the normal space condition. Specifically: 1. (T₁ condition) For any two distinct points $ x, y \in X $, there exists an open neighborhood of $ x $ not containing $ y $ and vice versa. 2. (Normal condition) For any two disjoint closed sets $ C $ and $ D $ in $ X $, there exist disjoint open sets $ U $ and $ V $ containing $ C $ and $ D $ respectively.

instT4SpaceOfT1SpaceOfNormalSpace instance

[T1Space X] [NormalSpace X] : T4Space X

Full source

instance (priority := 100) [T1Space X] [NormalSpace X] : T4Space X := ⟨⟩

Normal T₁ Spaces are T₄

Informal description

Every normal T₁ space is a T₄ space.

T4Space.t3Space instance

[T4Space X] : T3Space X

Full source

instance (priority := 100) T4Space.t3Space [T4Space X] : T3Space X where
  regular hs hxs := by simpa only [nhdsSet_singleton] using (normal_separation hs isClosed_singleton
    (disjoint_singleton_right.mpr hxs)).disjoint_nhdsSet

T₄ Spaces are T₃ Spaces

Informal description

Every T₄ space is a T₃ space.

Topology.IsClosedEmbedding.t4Space theorem

[TopologicalSpace Y] [T4Space Y] {f : X → Y} (hf : IsClosedEmbedding f) : T4Space X

Full source

/-- If the codomain of a closed embedding is a T₄ space, then so is the domain. -/
protected theorem Topology.IsClosedEmbedding.t4Space [TopologicalSpace Y] [T4Space Y] {f : X → Y}
    (hf : IsClosedEmbedding f) : T4Space X where
  toT1Space := hf.isEmbedding.t1Space
  toNormalSpace := hf.normalSpace

T₄ Property Preserved Under Closed Embeddings

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be a closed embedding. If $Y$ is a T₄ space, then $X$ is also a T₄ space.

Homeomorph.t4Space theorem

[TopologicalSpace Y] [T4Space X] (h : X ≃ₜ Y) : T4Space Y

Full source

protected theorem Homeomorph.t4Space [TopologicalSpace Y] [T4Space X] (h : X ≃ₜ Y) : T4Space Y :=
  h.symm.isClosedEmbedding.t4Space

T₄ Property Preserved Under Homeomorphism

Informal description

Let $X$ and $Y$ be topological spaces with $X$ being a T₄ space, and let $h: X \to Y$ be a homeomorphism. Then $Y$ is also a T₄ space.

ULift.instT4Space instance

[T4Space X] : T4Space (ULift X)

Full source

instance ULift.instT4Space [T4Space X] : T4Space (ULift X) := IsClosedEmbedding.uliftDown.t4Space

Lifted T₄ Space Preserves T₄ Property

Informal description

For any T₄ space $X$, the lifted space $\text{ULift}\, X$ is also a T₄ space.

SeparationQuotient.instNormalSpace instance

[NormalSpace X] : NormalSpace (SeparationQuotient X)

Full source

/-- The `SeparationQuotient` of a normal space is a normal space. -/
instance [NormalSpace X] : NormalSpace (SeparationQuotient X) where
  normal s t hs ht hd := separatedNhds_iff_disjoint.2 <| by
    rw [← disjoint_comap_iff surjective_mk, comap_mk_nhdsSet, comap_mk_nhdsSet]
    exact disjoint_nhdsSet_nhdsSet (hs.preimage continuous_mk) (ht.preimage continuous_mk)
      (hd.preimage mk)

Normality of the Separation Quotient of a Normal Space

Informal description

For any normal topological space $X$, its separation quotient is also a normal space.

CompletelyNormalSpace structure

(X : Type u) [TopologicalSpace X]

Full source

/-- A topological space `X` is a *completely normal space* provided that for any two sets `s`, `t`
such that if both `closure s` is disjoint with `t`, and `s` is disjoint with `closure t`,
then there exist disjoint neighbourhoods of `s` and `t`. -/
class CompletelyNormalSpace (X : Type u) [TopologicalSpace X] : Prop where
  /-- If `closure s` is disjoint with `t`, and `s` is disjoint with `closure t`, then `s` and `t`
  admit disjoint neighbourhoods. -/
  completely_normal :
    ∀ ⦃s t : Set X⦄, Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (𝓝ˢ s) (𝓝ˢ t)

Completely normal space

Informal description

A topological space $ X $ is called a *completely normal space* if for any two subsets $ s $ and $ t $ of $ X $ such that the closure of $ s $ is disjoint from $ t $ and $ s $ is disjoint from the closure of $ t $, there exist disjoint open neighborhoods of $ s $ and $ t $.

CompletelyNormalSpace.toNormalSpace instance

[CompletelyNormalSpace X] : NormalSpace X

Full source

/-- A completely normal space is a normal space. -/
instance (priority := 100) CompletelyNormalSpace.toNormalSpace
    [CompletelyNormalSpace X] : NormalSpace X where
  normal s t hs ht hd := separatedNhds_iff_disjoint.2 <|
    completely_normal (by rwa [hs.closure_eq]) (by rwa [ht.closure_eq])

Complete Normality Implies Normality

Informal description

Every completely normal topological space is a normal space.

Topology.IsEmbedding.completelyNormalSpace theorem

[TopologicalSpace Y] [CompletelyNormalSpace Y] {e : X → Y} (he : IsEmbedding e) : CompletelyNormalSpace X

Full source

theorem Topology.IsEmbedding.completelyNormalSpace [TopologicalSpace Y] [CompletelyNormalSpace Y]
    {e : X → Y} (he : IsEmbedding e) : CompletelyNormalSpace X := by
  refine ⟨fun s t hd₁ hd₂ => ?_⟩
  simp only [he.isInducing.nhdsSet_eq_comap]
  refine disjoint_comap (completely_normal ?_ ?_)
  · rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]
  · rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_right]

Embedding Preserves Complete Normality

Informal description

Let $Y$ be a completely normal topological space and $e : X \to Y$ be an embedding. Then $X$ is also a completely normal space.

instCompletelyNormalSpaceSubtype instance

[CompletelyNormalSpace X] {p : X → Prop} : CompletelyNormalSpace { x // p x }

Full source

/-- A subspace of a completely normal space is a completely normal space. -/
instance [CompletelyNormalSpace X] {p : X → Prop} : CompletelyNormalSpace { x // p x } :=
  IsEmbedding.subtypeVal.completelyNormalSpace

Subspaces of Completely Normal Spaces are Completely Normal

Informal description

For any completely normal topological space $X$ and any predicate $p$ on $X$, the subspace $\{x \in X \mid p(x)\}$ is also a completely normal space.

ULift.instCompletelyNormalSpace instance

[CompletelyNormalSpace X] : CompletelyNormalSpace (ULift X)

Full source

instance ULift.instCompletelyNormalSpace [CompletelyNormalSpace X] :
    CompletelyNormalSpace (ULift X) :=
  IsEmbedding.uliftDown.completelyNormalSpace

Complete Normality of Lifted Topological Spaces

Informal description

For any completely normal topological space $X$, the lifted space $\text{ULift}\, X$ is also completely normal.

T5Space structure

(X : Type u) [TopologicalSpace X] : Prop extends T1Space X, CompletelyNormalSpace X

Full source

/-- A T₅ space is a completely normal T₁ space. -/
class T5Space (X : Type u) [TopologicalSpace X] : Prop extends T1Space X, CompletelyNormalSpace X

T₅ space

Informal description

A topological space $X$ is called a T₅ space if it is a T₁ space and completely normal. This means that for any two subsets $s$ and $t$ of $X$ such that the closure of $s$ is disjoint from $t$ and $s$ is disjoint from the closure of $t$, there exist disjoint open neighborhoods of $s$ and $t$.

Topology.IsEmbedding.t5Space theorem

[TopologicalSpace Y] [T5Space Y] {e : X → Y} (he : IsEmbedding e) : T5Space X

Full source

theorem Topology.IsEmbedding.t5Space [TopologicalSpace Y] [T5Space Y] {e : X → Y}
    (he : IsEmbedding e) : T5Space X where
  __ := he.t1Space
  completely_normal := by
    have := he.completelyNormalSpace
    exact completely_normal

T₅ Space Property Preserved Under Embedding from T₅ Space

Informal description

Let $X$ and $Y$ be topological spaces, with $Y$ being a T₅ space. If $e: X \to Y$ is an embedding (a continuous injective map that is a homeomorphism onto its image), then $X$ is also a T₅ space.

Homeomorph.t5Space theorem

[TopologicalSpace Y] [T5Space X] (h : X ≃ₜ Y) : T5Space Y

Full source

protected theorem Homeomorph.t5Space [TopologicalSpace Y] [T5Space X] (h : X ≃ₜ Y) : T5Space Y :=
  h.symm.isClosedEmbedding.t5Space

T₅ Space Property Preserved Under Homeomorphism

Informal description

Let $X$ and $Y$ be topological spaces. If $X$ is a T₅ space and $h: X \to Y$ is a homeomorphism, then $Y$ is also a T₅ space.

T5Space.toT4Space instance

[T5Space X] : T4Space X

Full source

/-- A `T₅` space is a `T₄` space. -/
instance (priority := 100) T5Space.toT4Space [T5Space X] : T4Space X where

T₅ Spaces are T₄ Spaces

Informal description

Every T₅ space is a T₄ space.

instT5SpaceSubtype instance

[T5Space X] {p : X → Prop} : T5Space { x // p x }

Full source

/-- A subspace of a T₅ space is a T₅ space. -/
instance [T5Space X] {p : X → Prop} : T5Space { x // p x } :=
  IsEmbedding.subtypeVal.t5Space

Subspaces of T₅ Spaces are T₅

Informal description

For any T₅ space $X$ and any subset defined by a predicate $p : X \to \text{Prop}$, the subspace $\{x \in X \mid p(x)\}$ is also a T₅ space.

ULift.instT5Space instance

[T5Space X] : T5Space (ULift X)

Full source

instance ULift.instT5Space [T5Space X] : T5Space (ULift X) :=
  IsEmbedding.uliftDown.t5Space

T₅ Space Structure on ULift of a T₅ Space

Informal description

For any T₅ space $X$, the lifted space $\text{ULift}\, X$ is also a T₅ space.

instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space instance

[CompletelyNormalSpace X] [R0Space X] : T5Space (SeparationQuotient X)

Full source

/-- The `SeparationQuotient` of a completely normal R₀ space is a T₅ space. -/
instance [CompletelyNormalSpace X] [R0Space X] : T5Space (SeparationQuotient X) where
  t1 := by
    rwa [((t1Space_TFAE (SeparationQuotient X)).out 1 0 :), SeparationQuotient.t1Space_iff]
  completely_normal s t hd₁ hd₂ := by
    rw [← disjoint_comap_iff surjective_mk, comap_mk_nhdsSet, comap_mk_nhdsSet]
    apply completely_normal <;> rw [← preimage_mk_closure]
    exacts [hd₁.preimage mk, hd₂.preimage mk]

Separation Quotient of a Completely Normal R₀ Space is T₅

Informal description

For any topological space $X$ that is completely normal and R₀, the separation quotient of $X$ is a T₅ space.

connectedComponent_eq_iInter_isClopen theorem

[T2Space X] [CompactSpace X] (x : X) : connectedComponent x = ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s

Full source

/-- In a compact T₂ space, the connected component of a point equals the intersection of all
its clopen neighbourhoods. -/
theorem connectedComponent_eq_iInter_isClopen [T2Space X] [CompactSpace X] (x : X) :
    connectedComponent x = ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s := by
  apply Subset.antisymm connectedComponent_subset_iInter_isClopen
  -- Reduce to showing that the clopen intersection is connected.
  refine IsPreconnected.subset_connectedComponent ?_ (mem_iInter.2 fun s => s.2.2)
  -- We do this by showing that any disjoint cover by two closed sets implies
  -- that one of these closed sets must contain our whole thing.
  -- To reduce to the case where the cover is disjoint on all of `X` we need that `s` is closed
  have hs : @IsClosed X _ (⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s) :=
    isClosed_iInter fun s => s.2.1.1
  rw [isPreconnected_iff_subset_of_fully_disjoint_closed hs]
  intro a b ha hb hab ab_disj
  -- Since our space is normal, we get two larger disjoint open sets containing the disjoint
  -- closed sets. If we can show that our intersection is a subset of any of these we can then
  -- "descend" this to show that it is a subset of either a or b.
  rcases normal_separation ha hb ab_disj with ⟨u, v, hu, hv, hau, hbv, huv⟩
  obtain ⟨s, H⟩ : ∃ s : Set X, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v := by
    /- Now we find a clopen set `s` around `x`, contained in `u ∪ v`. We utilize the fact that
    `X \ u ∪ v` will be compact, so there must be some finite intersection of clopen neighbourhoods
    of `X` disjoint to it, but a finite intersection of clopen sets is clopen,
    so we let this be our `s`. -/
    have H1 := (hu.union hv).isClosed_compl.isCompact.inter_iInter_nonempty
      (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s) fun s => s.2.1.1
    rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1
    obtain ⟨si, H2⟩ :=
      H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau hbv)
    refine ⟨⋂ U ∈ si, Subtype.val U, ?_, ?_, ?_⟩
    · exact isClopen_biInter_finset fun s _ => s.2.1
    · exact mem_iInter₂.2 fun s _ => s.2.2
    · rwa [← disjoint_compl_left_iff_subset, disjoint_iff_inter_eq_empty,
        ← not_nonempty_iff_eq_empty]
  -- So, we get a disjoint decomposition `s = s ∩ u ∪ s ∩ v` of clopen sets. The intersection of all
  -- clopen neighbourhoods will then lie in whichever of u or v x lies in and hence will be a subset
  -- of either a or b.
  · have H1 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hu hv huv
    rw [union_comm] at H
    have H2 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hv hu huv.symm
    by_cases hxu : x ∈ u <;> [left; right]
    -- The x ∈ u case.
    · suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ u
        from Disjoint.left_le_of_le_sup_right hab (huv.mono this hbv)
      · apply Subset.trans _ s.inter_subset_right
        exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ u, H1, mem_inter H.2.1 hxu⟩
    -- If x ∉ u, we get x ∈ v since x ∈ u ∪ v. The rest is then like the x ∈ u case.
    · have h1 : x ∈ v :=
        (hab.trans (union_subset_union hau hbv) (mem_iInter.2 fun i => i.2.2)).resolve_left hxu
      suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ v
        from (huv.symm.mono this hau).left_le_of_le_sup_left hab
      · refine Subset.trans ?_ s.inter_subset_right
        exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ v, H2, mem_inter H.2.1 h1⟩

Connected Component as Intersection of Clopen Sets in Compact Hausdorff Spaces

Informal description

In a compact Hausdorff space $X$, the connected component of a point $x \in X$ is equal to the intersection of all clopen (both closed and open) subsets of $X$ that contain $x$. That is, \[ \text{connectedComponent}(x) = \bigcap_{\substack{s \subseteq X \\ \text{clopen}, x \in s}} s. \]

ConnectedComponents.t2 instance

[T2Space X] [CompactSpace X] : T2Space (ConnectedComponents X)

Full source

/-- `ConnectedComponents X` is Hausdorff when `X` is Hausdorff and compact -/
@[stacks 0900 "The Stacks entry proves profiniteness."]
instance ConnectedComponents.t2 [T2Space X] [CompactSpace X] : T2Space (ConnectedComponents X) := by
  -- Fix 2 distinct connected components, with points a and b
  refine ⟨ConnectedComponents.surjective_coe.forall₂.2 fun a b ne => ?_⟩
  rw [ConnectedComponents.coe_ne_coe] at ne
  have h := connectedComponent_disjoint ne
  -- write ↑b as the intersection of all clopen subsets containing it
  rw [connectedComponent_eq_iInter_isClopen b, disjoint_iff_inter_eq_empty] at h
  -- Now we show that this can be reduced to some clopen containing `↑b` being disjoint to `↑a`
  obtain ⟨U, V, hU, ha, hb, rfl⟩ : ∃ (U : Set X) (V : Set (ConnectedComponents X)),
      IsClopen U ∧ connectedComponent a ∩ U = ∅ ∧ connectedComponent b ⊆ U ∧ (↑) ⁻¹' V = U := by
    have h :=
      (isClosed_connectedComponent (α := X)).isCompact.elim_finite_subfamily_closed
        _ (fun s : { s : Set X // IsClopen s ∧ b ∈ s } => s.2.1.1) h
    obtain ⟨fin_a, ha⟩ := h
    -- This clopen and its complement will separate the connected components of `a` and `b`
    set U : Set X := ⋂ (i : { s // IsClopen s ∧ b ∈ s }) (_ : i ∈ fin_a), i
    have hU : IsClopen U := isClopen_biInter_finset fun i _ => i.2.1
    exact ⟨U, (↑) '' U, hU, ha, subset_iInter₂ fun s _ => s.2.1.connectedComponent_subset s.2.2,
      (connectedComponents_preimage_image U).symm ▸ hU.biUnion_connectedComponent_eq⟩
  rw [ConnectedComponents.isQuotientMap_coe.isClopen_preimage] at hU
  refine ⟨Vᶜ, V, hU.compl.isOpen, hU.isOpen, ?_, hb mem_connectedComponent, disjoint_compl_left⟩
  exact fun h => flip Set.Nonempty.ne_empty ha ⟨a, mem_connectedComponent, h⟩

Hausdorff Property of Connected Components in Compact Hausdorff Spaces

Informal description

For any Hausdorff and compact topological space $X$, the space of connected components $\text{ConnectedComponents}(X)$ is also Hausdorff.

Mathlib.Topology.Separation.Regular

Main definitions

Main results

Regular spaces

T₃ spaces

References