Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)
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 compact Hausdorff space is regular and normal, hence T3T_3 and T4T_4

Statement

Let XX be a compact (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not) topological space. Then:

  1. XX is regular (Regular spaces and T3T_3 spaces, with the source disagreement over whether regularity includes T1T_1 stated explicitly);
  2. XX is normal (Normal spaces and T4T_4 spaces, with the source disagreement over whether normality includes T1T_1 stated explicitly);
  3. XX is T1T_1 (T0T_0 (Kolmogorov) and T1T_1 (Frechet) spaces), and hence XX is T3T_3 and T4T_4.

Following Regular spaces and T3T_3 spaces, with the source disagreement over whether regularity includes T1T_1 stated explicitly and Normal spaces and T4T_4 spaces, with the source disagreement over whether normality includes T1T_1 stated explicitly, regular and normal name the separation conditions alone and the numerals T3T_3 and T4T_4 name their conjunctions with T1T_1; claim 3 is what supplies the T1T_1 half, and it is stated separately for that reason.

Nothing stronger is claimed. In particular it is not asserted here that a compact Hausdorff space is completely regular (Regular spaces and T3T_3 spaces, with the source disagreement over whether regularity includes T1T_1 stated explicitly distinguishes the two conditions), and no continuous real-valued function is produced anywhere below.

Facts & Assumptions

Given: A compact Hausdorff topological space XX.

[A1]

XX is regular when for every closed CXC \subseteq X and every xXCx \in X \setminus C there are disjoint open UxU \ni x and VCV \supseteq C; the case C=C = \varnothing is met by U=XU = X and V=V = \varnothing, and T3T_3 is regular together with T1T_1 (Regular spaces and T3T_3 spaces, with the source disagreement over whether regularity includes T1T_1 stated explicitly, T0T_0 (Kolmogorov) and T1T_1 (Frechet) spaces).

[A2]

XX is normal when for all disjoint closed A,BXA, B \subseteq X there are disjoint open UAU \supseteq A and VBV \supseteq B; the cases A=A = \varnothing and B=B = \varnothing are met by \varnothing together with XX, and T4T_4 is normal together with T1T_1 (Normal spaces and T4T_4 spaces, with the source disagreement over whether normality includes T1T_1 stated explicitly, T0T_0 (Kolmogorov) and T1T_1 (Frechet) spaces).

[A3]

XX is a topological space, so a subset is closed exactly when its complement is open (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Proof

technique · direct
1.1

Let CXC \subseteq X be closed and let xXCx \in X \setminus C; since XX is compact and CC is closed in XX, the subspace CC is compact, and xx does not lie in it.

A3L1
1.2

Let A,BXA, B \subseteq X be closed with AB=A \cap B = \varnothing; since XX is compact and both are closed in XX, both subspaces AA and BB are compact.

A3L1
1.3

XX is T1T_1, being Hausdorff.

L3
2.1

By [L2], applied to the point xx and the disjoint compact set CC of step 1.1, there are disjoint open UxU \ni x and VCV \supseteq C; as CC and xx were arbitrary this is exactly the condition of [A1], so XX is regular, which is claim 1.

step 1.1A1L2
2.2

By [L2], applied to the two disjoint compact sets AA and BB of step 1.2, there are disjoint open UAU \supseteq A and VBV \supseteq B; as AA and BB were arbitrary this is the condition of [A2], so XX is normal, which is claim 2.

step 1.2A2L2
3.1

By step 1.3 the space is T1T_1; with step 2.1 it is regular and T1T_1, hence T3T_3, and with step 2.2 it is normal and T1T_1, hence T4T_4. This is claim 3.

step 1.3step 2.1step 2.2A1A2
4.1

Steps 2.1, 2.2 and 3.1 are claims 1, 2 and 3, so a compact Hausdorff space is regular, normal, T3T_3 and T4T_4.

step 2.1step 2.2step 3.1

Remarks

  • The whole content is that "closed" and "compact" coincide here, in the direction that is needed. Regularity asks a point to be separated from a closed set and normality asks two closed sets to be separated; compactness of the ambient space converts each closed set into a compact one, and the separation of compact sets in a Hausdorff space is what In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones supplies. No new separation argument is run.

  • Why compactness of XX is needed and not just of the sets separated. The hypothesis is used only through [L1], to know that an arbitrary closed subset of XX is compact. A Hausdorff space in which the sets to be separated happen to be compact is separated by [L2] alone and needs no hypothesis on the ambient space at all; what compactness of XX buys is that every closed set is such a set.

  • The degenerate cases are not a gap. If CC, AA or BB is empty the required open sets are named outright in [A1] and [A2], so the argument does not depend on any nonemptiness hidden in the compact-separation clauses.

Depends on

Used by

Dependency tree · next 3 levels

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