Alphabeta Math
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.

In a metric space every closed set is a zero set and a Gδ, 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 ι(n+1) of R (The canonical natural ι(n)=n⋅1F of a field). Then:

  1. Every closed set is a zero set. For closed C⊆X there is a continuous f:X→R with C=Z(f) (Zero sets and cozero sets of continuous real-valued functions); for C≠∅ 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=∅ the constant function 1.
  2. Every closed set is a Gδ (Gδ and Fσ subsets of a topological space, agreeing with the real-line notion): for C≠∅, C  =  ⋂n∈N{ x∈X:d(x,C)<1/(n+1) }, an intersection of open sets, and ∅ is open hence a Gδ.
  3. X is completely regular (Completely regular spaces and Tychonoff (T312) spaces): for closed C and x0∉C the function f(x):=min⁡{1, d(x,C)/r} with r:=d(x0,C) is continuous, takes the value 1 at x0 and the value 0 on C, when C≠∅; for C=∅ the constant function 1 serves.
  4. 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 T6, T5, T4, T312, T3, T212, T2, T1 and T0.

No choice principle is used anywhere below.

Facts & Assumptions

Given: A metric space (X,d), a closed set C⊆X, a point x0∈X∖C, and R with its usual topology.

[L2]

∣d(x,S)−d(y,S)∣≤d(x,y) for nonempty S (∣d(x,A)−d(y,A)∣≤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)∣≤L d(x,y) with L>0 is continuous in the ε-δ sense, by δ:=ε/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 ε-δ form, Metric continuity characterisations, with countable choice for the sequential converse, clause (b), Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).

[L5]

For every real ε>0 there is a natural k≥1 with 1/k<ε, and every nonzero natural is a successor, so k=n+1 for some n∈N (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every nonzero natural number is a successor, The canonical natural ι(n)=n⋅1F 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≤t≤1 (Intervals of R: the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct
1.1

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

L1L2L3assume-hyp
1.2

If C=∅ then the constant function 1 is continuous and has zero set ∅=C, since 1≠0.

L3L4
2.1

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

step 1.1L1L4
2.2

Under step 1.1: for each n the set Wn:={ x:d(x,C)<1/(n+1) } is open, since for x∈Wn and t:=1/(n+1)−d(x,C)>0 any y with d(x,y)<t has d(y,C)≤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⊆⋂nWn, since d(x,C)=0<1/(n+1) for x∈C by [L1] and step 2.1.

step 2.1step 2.2L1
3.3

Under step 1.1: if x∉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∉Wn.

step 2.1step 2.2L1L5
3.4

Under step 1.1 with x0∉C: r:=d(x0,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=⋂nWn for nonempty closed C, and ∅ is open hence a Gδ by [L4]; this is claim 2.

step 3.2step 3.3L4
4.2

Under step 3.4: ∣min⁡{1,u}−min⁡{1,v}∣≤∣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≤1<v then the left side is 1−u, which is at most v−u, the remaining case v≤1<u being the same with u and v exchanged; hence ∣f(x)−f(y)∣≤∣d(x,C)−d(y,C)∣/r≤d(x,y)/r and f is continuous by [L3] with L=1/r.

step 3.4L2L3L6
4.3

Under step 3.4: f(x0)=min⁡{1,r/r}=min⁡{1,1}=1, and f(y)=min⁡{1,0}=0 for y∈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=∅, 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 T1 by [L7], so it is Tychonoff; it is normal by [L8] and every closed subset of it is a Gδ by step 4.1, so it is perfectly normal.

step 4.1step 5.1L7L8
7.1

Being perfectly normal and T1, such a Y is T6; it is T5 and T4 by [L8] and T1, it is T312 by step 6.1, and it is T3, T212, T2, T1 and T0 by the implications already proved on this page; this is claim 4.

step 6.1L7L8∎

Remarks

Depends on

Used by

Dependency tree · two levels

81 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