Regular Space

Statement

A topological space $X$ is regular if for every closed set $C$ and every point $p \notin C$ there exist disjoint open sets $U \supseteq C$ and $V \ni p$:

A $T_3$ space is regular + $T_1$ (points are closed). Every metric space is regular: the distance function $d(p, C) > 0$ provides explicit separating balls.

Visualization

Point $p$ outside closed set $C$ — disjoint open neighborhoods:

Topological space X:

   C (closed)           p (point not in C)
   ╭──────────╮                ●
  /            \
 │  ████████   │             / ← V open, contains p
 │  ████████   │           ╭───╮
 │  ████████   │           │ p │
  \            /           ╰───╯
   ╰──────────╯
    ↑
    U open, contains C
    U ∩ V = ∅

In ℝ (metric space):  C = [2, 5],  p = 0
  d(p, C) = 2
  U = (1, 6)   ← contains C
  V = (−1, 1)  ← contains p
  U ∩ V = ∅ ✓

Separation hierarchy:

T₀ (Kolmogorov)
  ↓
T₁ (Fréchet) — points are closed
  ↓
T₂ (Hausdorff) — distinct points have disjoint neighborhoods
  ↓
T₃ = Regular + T₁ — point vs. closed set separated
  ↓
T₄ = Normal + T₁ — closed set vs. closed set separated
  ↓
T₆ = Perfectly normal + T₁

Proof Sketch

Uniform spaces (hence metric spaces) are regular:

1. Let $C \subseteq X$ be closed and $p \notin C$, so $p \in X \setminus C$ (open).
2. By the uniform space axioms there exists an entourage $E$ with $E[p] \cap C = \emptyset$ (since $C^c$ is open in the uniform topology).
3. Set $V = \text{int}(E[p])$ and $U = X \setminus \overline{E^{-1}[p]^c}$. Symmetry of $E$ ensures $U \supseteq C$ and $U \cap V = \emptyset$.
4. In metric spaces: choose $r = d(p, C)/2$; then $V = B_r(p)$ and $U = \{x : d(x, C) < r\}$ work directly.

Mathlib formalizes this as: UniformSpace.to_regularSpace, promoted automatically whenever a UniformSpace instance exists.

Connections

• Normal SpaceNormal Space$$\forall\, F,G\text{ closed}, F\cap G=\emptyset:\;\exists\,U\supseteq F,\,V\supseteq G\text{ open},\;U\cap V=\emptyset$$A topological space is normal if disjoint closed sets can be separated by disjoint open neighborhoodsRead more → — every normal space ($T_4$) is regular ($T_3$); regularity is the weaker point-vs-set separation while normality handles set-vs-set.
• Heine–Borel TheoremHeine–Borel Theorem$$K \subseteq \mathbb{R}^n \;\text{compact} \iff K \;\text{closed and bounded}$$In ℝⁿ, a subset is compact if and only if it is closed and boundedRead more → — compact Hausdorff spaces are regular (in fact normal); Heine–Borel's compact sets in $\mathbb{R}^n$ inherit regularity from the Euclidean metric.
• Urysohn's LemmaUrysohn's Lemma$$\exists\, f : X \to [0,1],\quad f|_s = 0,\; f|_t = 1$$In a normal space, disjoint closed sets can be separated by a continuous functionRead more → — Urysohn's lemma applies to normal spaces; regular + second-countable implies normal (by Urysohn's metrization argument), so the two separation axioms interact closely.
• Metrizable SpacesMetrizable Spaces$$\exists\, d:\, X\times X\to\mathbb{R}_{\ge 0},\;\tau = \tau_d$$A topological space is metrizable if its topology is induced by some metricRead more → — metrizable spaces are exactly those that are regular, Hausdorff, and second-countable (Urysohn metrization theorem); regularity is one of the three equivalent conditions.

import Mathlib.Topology.UniformSpace.Separation

/-- Every uniform space is regular.
    Mathlib instance: `UniformSpace.to_regularSpace`. -/
theorem uniformSpace_regular
    {X : Type*} [UniformSpace X] : RegularSpace X :=
  inferInstance

/-- In particular, every (pseudo-)metric space is regular. -/
example : RegularSpace ℝ := inferInstance