TheoremStatement: AI-adaptedProof: AI-generatedprecheck 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.

A normal $T_{1}$ space is regular, hence $T_{3}$ , hence Urysohn, Hausdorff, $T_{1}$ and $T_{0}$

Statement

Let $(X, T)$ be a $T_{4}$ space, that is a normal $T_{1}$ space (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly, $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces). Then $X$ is regular (Regular spaces and $T_{3}$ spaces, with the source disagreement over whether regularity includes $T_{1}$ stated explicitly), hence $T_{3}$ , and therefore also Urysohn (Urysohn ( $T_{2 \frac{1}{2}}$ ) space: distinct points have neighbourhoods with disjoint closures), Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not), $T_{1}$ and $T_{0}$ .

The $T_{1}$ hypothesis is not decoration. Normality alone implies none of the conclusions: the indiscrete topology on a two-point set is normal and not even $T_{0}$ , which is recorded among this page's false statements.

Facts & Assumptions

Given: A topological space $(X, T)$ that is normal and $T_{1}$ , a closed set $C \subseteq X$ and a point $x \in X ∖ C$ .

[A1]

Normality: disjoint closed sets admit disjoint open supersets (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

[A2]

$X$ is regular when a point and a closed set not containing it admit disjoint open supersets; $T_{3}$ means regular and $T_{1}$ (Regular spaces and $T_{3}$ spaces, with the source disagreement over whether regularity includes $T_{1}$ stated explicitly).

[L1]

In a $T_{1}$ space every singleton is closed (A space is $T_{1}$ if and only if every singleton is closed, if and only if every finite subset is closed, if and only if its topology contains the cofinite topology, clause (b)).

[L2]

Every regular $T_{1}$ space is Urysohn, every Urysohn space is Hausdorff, and every Hausdorff space is $T_{1}$ and hence $T_{0}$ (Every Urysohn space is Hausdorff, every Hausdorff space is $T_{1}$ and hence $T_{0}$ , and every regular $T_{1}$ space is Urysohn).

Proof

technique · direct

1.1

${x}$ is closed, since $X$ is $T_{1}$ .

1.2

${x} \cap C = \emptyset$ , since $x \notin C$ .

given

2.1

By [A1] applied to the disjoint closed sets ${x}$ and $C$ there are disjoint open $U \supseteq {x}$ and $V \supseteq C$ ; in particular $x \in U$ .

step 1.1step 1.2A1

3.1

Since $C$ and $x \notin C$ were arbitrary, step 2.1 shows that $X$ is regular; being also $T_{1}$ , it is $T_{3}$ .

step 2.1A2

4.1

By [L2] the space $X$ is Urysohn, hence Hausdorff, hence $T_{1}$ and $T_{0}$ ; with step 3.1 this is the whole statement.

step 3.1L2∎

Remarks

The proof is one line and the hypothesis does all the work. Normality separates two closed sets; the $T_{1}$ hypothesis is exactly what turns the point into one of them. This is the pattern of every " $T_{n + 1}$ implies $T_{n}$ " argument in the chain, and it is why this library never builds $T_{1}$ silently into the words regular and normal (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).
The converse is not proved here and is not asserted. Whether a $T_{3}$ space must be normal is left open on this page: every witness reachable from this page's material would need machinery it does not have, so no false statement asserting a reversal is planted here (Conventions on this page, and the one implication of the classical chain that is not available at this point in the reading order).

Depends on

Used by

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Normal space (Wikipedia) (standard reference, not scraped)
Separation axiom (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §32 (standard reference, not scraped)
Urysohn and completely Hausdorff spaces (Wikipedia) (standard reference, not scraped)

A normal T1T1​ space is regular, hence T3T3​, hence Urysohn, Hausdorff, T1T1​ and T0T0​