TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

In a metric space every closed set is a zero set and a $G_\delta$ , and the distance function separates a point from a closed set, so every metrizable space is Tychonoff and perfectly normal

Statement

Let $(X,d)$ be a metric space (Metric space: $d(x,y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric) with its metric topology (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement), and write $1/(n+1)$ for the inverse of the canonical natural $\iota(n+1)$ of $\mathbb{R}$ (The canonical natural $\iota(n) = n \cdot 1_F$ of a field). Then:

Every closed set is a zero set. For closed $C \subseteq X$ there is a continuous $f : X \to \mathbb{R}$ with $C = Z(f)$ (Zero sets and cozero sets of continuous real-valued functions); for $C \ne \varnothing$ one may take $f(x) = d(x,C)$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space), and for $C = \varnothing$ the constant function $1$ .
Every closed set is a $G_\delta$ ( $G_\delta$ and $F_\sigma$ subsets of a topological space, agreeing with the real-line notion): for $C \ne \varnothing$ , $C \;=\; \bigcap_{n \in \mathbb{N}} \{\, x \in X : d(x,C) < 1/(n+1) \,\},$ an intersection of open sets, and $\varnothing$ is open hence a $G_\delta$ .
$X$ is completely regular (Completely regular spaces and Tychonoff ( $T_{3\frac{1}{2}}$ ) spaces): for closed $C$ and $x_0 \notin C$ the function $f(x) := \min\{1,\ d(x,C)/r\}$ with $r := d(x_0,C)$ is continuous, takes the value $1$ at $x_0$ and the value $0$ on $C$ , when $C \ne \varnothing$ ; for $C = \varnothing$ the constant function $1$ serves.
Consequently every metrizable space (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not) is Tychonoff and perfectly normal, and hence $T_6$ , $T_5$ , $T_4$ , $T_{3\frac12}$ , $T_3$ , $T_{2\frac12}$ , $T_2$ , $T_1$ and $T_0$ .

No choice principle is used anywhere below.

Facts & Assumptions

Given: A metric space $(X,d)$ , a closed set $C \subseteq X$ , a point $x_0 \in X \setminus C$ , and $\mathbb{R}$ with its usual topology.

[L1]

For nonempty $S \subseteq X$ the distance $d(x,S)$ is defined, is $\ge 0$ , and $\overline{S} = \{\, x : d(x,S) = 0 \,\}$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, The closure of a nonempty $A$ is $\{x : d(x,A) = 0\}$ , equals $A$ together with its limit points, and is the smallest closed superset, claim 1).

[L2]

$|d(x,S) - d(y,S)| \le d(x,y)$ for nonempty $S$ ( $|d(x,A) - d(y,A)| \le d(x,y)$ , so the distance to a fixed nonempty set is $1$ -Lipschitz).

[L3]

A map between metric spaces satisfying an inequality $|g(x) - g(y)| \le L\, d(x,y)$ with $L > 0$ is continuous in the $\varepsilon$ - $\delta$ sense, by $\delta := \varepsilon / L$ , and is therefore continuous as a map of topological spaces (Continuity of a map between metric spaces, at a point and globally, in the $\varepsilon$ - $\delta$ form, For a map of metric spaces the following agree: $\varepsilon$ - $\delta$ continuity everywhere, preimages of open sets are open, preimages of closed sets are closed, sequential continuity, and $f(\overline{A}) \subseteq \overline{f(A)}$ , clause (b), Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).

[L4]

A set is closed exactly when it equals its closure (The closure of a nonempty $A$ is $\{x : d(x,A) = 0\}$ , equals $A$ together with its limit points, and is the smallest closed superset, claim 3); $\varnothing$ and $X$ are open (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L5]

For every real $\varepsilon > 0$ there is a natural $k \ge 1$ with $1/k < \varepsilon$ , and every nonzero natural is a successor, so $k = n+1$ for some $n \in \mathbb{N}$ (For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ , Every nonzero natural number is a successor, The canonical natural $\iota(n) = n \cdot 1_F$ of a field).

[L6]

A two-element set of reals has a maximum and a minimum, each of which is one of the two elements (Maximum and minimum of a set, Every nonempty finite set of reals has a maximum and a minimum); and $[0,1]$ is the set of reals $t$ with $0 \le t \le 1$ (Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length).

[L7]

Every metrizable space is Hausdorff, hence $T_1$ and $T_0$ (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not, Every Urysohn space is Hausdorff, every Hausdorff space is $T_1$ and hence $T_0$ , and every regular $T_1$ space is Urysohn, $T_0$ (Kolmogorov) and $T_1$ (Frechet) spaces).

[L8]

Every metric space is completely normal, hence normal (In a metric space any two separated sets have disjoint open neighbourhoods, so every metrizable space is completely normal).

Proof

technique · direct

1.1

Suppose $C \ne \varnothing$ and put $g(x) := d(x,C)$ ; then $g$ is continuous by [L2] and [L3] with $L = 1$ .

L1L2L3assume-hyp

1.2

If $C = \varnothing$ then the constant function $1$ is continuous and has zero set $\varnothing = C$ , since $1 \ne 0$ .

L3L4

2.1

Under step 1.1: $Z(g) = \{\, x : d(x,C) = 0 \,\} = \overline{C} = C$ , the last equality because $C$ is closed.

step 1.1L1L4

2.2

Under step 1.1: for each $n$ the set $W_n := \{\, x : d(x,C) < 1/(n+1) \,\}$ is open, since for $x \in W_n$ and $t := 1/(n+1) - d(x,C) > 0$ any $y$ with $d(x,y) < t$ has $d(y,C) \le d(x,C) + d(x,y) < 1/(n+1)$ by [L2].

step 1.1L2

3.1

By steps 2.1 and 1.2 every closed subset of $X$ is a zero set, which is claim 1.

step 2.1step 1.2

3.2

Under step 1.1: $C \subseteq \bigcap_n W_n$ , since $d(x,C) = 0 < 1/(n+1)$ for $x \in C$ by [L1] and step 2.1.

step 2.1step 2.2L1

3.3

Under step 1.1: if $x \notin C$ then $d(x,C) > 0$ by [L1] and step 2.1, so [L5] gives $n$ with $1/(n+1) < d(x,C)$ and hence $x \notin W_n$ .

step 2.1step 2.2L1L5

3.4

Under step 1.1 with $x_0 \notin C$ : $r := d(x_0,C) > 0$ by [L1] and step 2.1, and $f(x) := \min\{1,\ d(x,C)/r\}$ takes values in $[0,1]$ by [L1] and [L6].

step 2.1L1L6

4.1

Steps 3.2 and 3.3 give $C = \bigcap_n W_n$ for nonempty closed $C$ , and $\varnothing$ is open hence a $G_\delta$ by [L4]; this is claim 2.

step 3.2step 3.3L4

4.2

Under step 3.4: $|\min\{1,u\} - \min\{1,v\}| \le |u - v|$ for all reals $u,v$ , since if both are at most $1$ the two sides are equal, if both exceed $1$ the left side is $0$ , and if $u \le 1 < v$ then the left side is $1 - u$ , which is at most $v - u$ , the remaining case $v \le 1 < u$ being the same with $u$ and $v$ exchanged; hence $|f(x) - f(y)| \le |d(x,C) - d(y,C)|/r \le d(x,y)/r$ and $f$ is continuous by [L3] with $L = 1/r$ .

step 3.4L2L3L6

4.3

Under step 3.4: $f(x_0) = \min\{1, r/r\} = \min\{1,1\} = 1$ , and $f(y) = \min\{1, 0\} = 0$ for $y \in C$ since $d(y,C) = 0$ .

step 3.4L1L6

5.1

By steps 4.2 and 4.3, and by step 1.2 for the case $C = \varnothing$ , the space $X$ is completely regular, which is claim 3.

step 1.2step 4.2step 4.3

6.1

A metrizable space $Y$ is completely regular by step 5.1 applied to any inducing metric, and it is $T_1$ by [L7], so it is Tychonoff; it is normal by [L8] and every closed subset of it is a $G_\delta$ by step 4.1, so it is perfectly normal.

step 4.1step 5.1L7L8

7.1

Being perfectly normal and $T_1$ , such a $Y$ is $T_6$ ; it is $T_5$ and $T_4$ by [L8] and $T_1$ , it is $T_{3\frac12}$ by step 6.1, and it is $T_3$ , $T_{2\frac12}$ , $T_2$ , $T_1$ and $T_0$ by the implications already proved on this page; this is claim 4.

step 6.1L7L8∎

Remarks

Claim 1 is the sharp form and claim 2 is its shadow. A zero set is always a $G_\delta$ (Zero sets and cozero sets of continuous real-valued functions), so claim 2 follows from claim 1; it is proved separately here because the explicit presentation $\bigcap_n \{x : d(x,C) < 1/(n+1)\}$ is the one quoted later, and because it makes visible that the index runs from $n = 0$ , where the radius is $1$ .
The empty closed set is not a nuisance to be waved away. $d(x,\varnothing)$ is undefined in this library, there being no infimum of the empty set (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space), so each of the three claims is discharged separately at $C = \varnothing$ by a constant function or by openness.
What this does not prove. It says nothing about which non-metrizable spaces are perfectly normal, and it gives no metrization theorem in the other direction: exhibiting a metric is the only way a space is shown metrizable here (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 129 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Normal space (Wikipedia) (standard reference, not scraped)
Tychonoff space (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §33 (standard reference, not scraped)
Metrizable space (Wikipedia) (standard reference, not scraped)
Gδ set (Wikipedia) (standard reference, not scraped)

In a metric space every closed set is a zero set and a GδG_\deltaGδ​, and the distance function separates a point from a closed set, so every metrizable space is Tychonoff and perfectly normal