Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Every completely regular space is regular, and every Tychonoff space is T3T_3

Statement

Let (X,T)(X, \mathcal{T}) be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). If XX is completely regular (Completely regular spaces and Tychonoff (T312T_{3\frac{1}{2}}) spaces) then XX is regular (Regular spaces and T3T_3 spaces, with the source disagreement over whether regularity includes T1T_1 stated explicitly). Consequently every Tychonoff space is T3T_3, being completely regular and T1T_1 (T0T_0 (Kolmogorov) and T1T_1 (Frechet) spaces).

This page does not prove the converse and does not assert it: a regular space that is not completely regular would need a construction this page does not carry, so whether the implication reverses is left open here.

Facts & Assumptions

Given: A completely regular space (X,T)(X,\mathcal{T}), a closed set CXC \subseteq X and a point x0XCx_0 \in X \setminus C.

[A1]

Complete regularity supplies a continuous f:X[0,1]f : X \to [0,1] with f(x0)=1f(x_0) = 1 and f(y)=0f(y) = 0 for every yCy \in C (Completely regular spaces and Tychonoff (T312T_{3\frac{1}{2}}) spaces).

[A2]

XX is regular when every such pair (C,x0)(C, x_0) admits disjoint open Ux0U \ni x_0 and VCV \supseteq C (Regular spaces and T3T_3 spaces, with the source disagreement over whether regularity includes T1T_1 stated explicitly).

[L1]

A map into the subspace [0,1][0,1] of R\mathbb{R} is continuous exactly when it is continuous as a map into R\mathbb{R}, and the open subsets of [0,1][0,1] are the traces on [0,1][0,1] of the open subsets of R\mathbb{R} (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace, Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct
1.1

Fix ff as in [A1], and put W1:=(1/2,)[0,1]W_1 := (1/2,\infty) \cap [0,1] and W0:=(,1/2)[0,1]W_0 := (-\infty,1/2) \cap [0,1], which are open in [0,1][0,1] and disjoint by [L1] and [L3].

A1L1L3
1.2

Put U:=f1[W1]U := f^{-1}[W_1] and V:=f1[W0]V := f^{-1}[W_0]; both are open in XX by [L2].

A1L2
2.1

x0Ux_0 \in U, since f(x0)=1>1/2f(x_0) = 1 > 1/2 and 1[0,1]1 \in [0,1].

step 1.1step 1.2A1L3
2.2

CVC \subseteq V, since f(y)=0<1/2f(y) = 0 < 1/2 and 0[0,1]0 \in [0,1] for every yCy \in C.

step 1.1step 1.2A1L3
2.3

UV=U \cap V = \varnothing: a point of both would satisfy f(x)>1/2f(x) > 1/2 and f(x)<1/2f(x) < 1/2, which is impossible by trichotomy of the order of R\mathbb{R}.

step 1.1step 1.2L3
3.1

By steps 1.2, 2.1, 2.2 and 2.3 the pair (C,x0)(C, x_0) is separated by disjoint open sets, and since CC and x0x_0 were arbitrary, XX is regular by [A2].

step 1.2step 2.1step 2.2step 2.3A2
4.1

If in addition XX is T1T_1 then XX is regular and T1T_1, that is T3T_3; so every Tychonoff space is T3T_3.

step 3.1A2

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 83 results over 16 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