Normal Space

Statement

A topological space $X$ is normal (a $T_4$ space when also $T_1$) if for every pair of disjoint closed sets $F$ and $G$ there exist disjoint open sets $U \supseteq F$ and $V \supseteq G$:

Every metric space is normal — the distance function $d(x, F)$ provides explicit separating open sets.

Visualization

Two disjoint closed disks in $\mathbb{R}^2$ — explicit separating opens:

ℝ² plane (normal space via Euclidean metric):

   F = closed disk of radius 1 at (-2, 0)
   G = closed disk of radius 1 at (+2, 0)

   distance from F:  d(x, F) = max(0, |x - (-2,0)| - 1)
   distance from G:  d(x, G) = max(0, |x - (+2,0)| - 1)

        U (open, contains F)       V (open, contains G)
          ╭──────────╮           ╭──────────╮
         /    ╭────╮  \         /  ╭────╮    \
        │    │  F  │   │       │  │  G  │    │
        │    │  ●  │   │       │  │  ●  │    │
         \    ╰────╯  /         \  ╰────╯    /
          ╰──────────╯           ╰──────────╯
               │ ← gap ─────────────────────────
               U = {x : d(x,F) < 1/2}       V = {x : d(x,G) < 1/2}

  U ∩ V = ∅  since  d(F,G) = 2 > 1/2 + 1/2 = 1

Normal vs. not normal:

Space	Normal?	Reason
$\mathbb{R}^n$ (metric)	yes	metric separation
$[0,1]$	yes	compact Hausdorff
$\mathbb{Q}$ (subspace of $\mathbb{R}$)	yes	metrizable
Long line	no	not normal ($T_3$ but not $T_4$)
Niemytzki plane	no	normal but not perfectly normal

Proof Sketch

Metric spaces are normal:

1. For disjoint closed sets $F, G \subseteq X$ (metric space), define $f(x) = d(x,F)/(d(x,F) + d(x,G))$.
2. The denominator is positive since $F \cap G = \emptyset$: if $d(x,F) = 0$ then $x \in F$ (closed), so $d(x,G) > 0$.
3. $f$ is continuous, $f|_F = 0$, $f|_G = 1$.
4. Set $U = f^{-1}([0, 1/2))$ and $V = f^{-1}((1/2, 1])$; both open, disjoint, and contain $F$, $G$ respectively.

This is precisely what Urysohn's lemma formalizes, and it shows metrizable $\Rightarrow$ normal.

Connections

• 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 is the precise statement that in a normal space one can find a continuous real-valued function separating any two disjoint closed sets; normality is the exact hypothesis needed.
• Regular SpaceRegular Space$$\forall\,C\text{ closed},\, p\notin C:\;\exists\,U\supseteq C,\,V\ni p\text{ open},\;U\cap V=\emptyset$$A topological space is regular if a closed set and a disjoint point can be separated by open neighborhoodsRead more → — normality strengthens regularity: regular spaces separate a point from a closed set; normal spaces separate two closed sets. Every metric space satisfies both.
• 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 normal ($T_4$); Heine–Borel identifies the compact sets in $\mathbb{R}^n$ where normality applies.
• Tychonoff's TheoremTychonoff's Theorem$$\prod_{i \in I} X_i \text{ compact} \iff \forall i,\; X_i \text{ compact}$$An arbitrary product of compact spaces is compact in the product topologyRead more → — a product of normal spaces need not be normal in general; Tychonoff's theorem compactifies, and compact Hausdorff spaces are always normal.

import Mathlib.Topology.GDelta.MetrizableSpace

/-- Every pseudo-metrizable space is normal.
    Mathlib: the instance `[PseudoMetrizableSpace X] : NormalSpace X`
    lives in `Mathlib.Topology.GDelta.MetrizableSpace`. -/
theorem pseudoMetrizable_normal
    {X : Type*} [TopologicalSpace X] [PseudoMetrizableSpace X] : NormalSpace X :=
  inferInstance