CorollaryStatement: AI-adaptedProof: AI-generatedSession-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.

Under dependent choice a compact Hausdorff space is Tychonoff, and its disjoint closed sets are separated by continuous functions

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$ -indexed chain). Let $(X,\mathcal{T})$ be compact (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) and Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not). Then $X$ is Tychonoff (Completely regular spaces and Tychonoff ( $T_{3\frac{1}{2}}$ ) spaces), and any two disjoint closed subsets of $X$ are separated by a continuous function into $[0,1]$ in the sense of Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0,1]$ , and conversely such a space is normal.

Facts & Assumptions

Given: A compact Hausdorff topological space $(X,\mathcal{T})$ , and dependent choice.

[L1]

A compact Hausdorff space is regular and normal, hence $T_3$ and $T_4$ (A compact Hausdorff space is regular and normal, hence $T_3$ and $T_4$ ).

[L2]

Under dependent choice, a normal $T_1$ space is completely regular (Under dependent choice a normal $T_1$ space is completely regular, so $T_4 \Rightarrow T_{3\frac{1}{2}}$ , and together with the implications already proved this is the whole classical chain).

[L3]

Under dependent choice, if $X$ is normal and $P,Q \subseteq X$ are disjoint closed sets, there is a continuous $f : X \to [0,1]$ with $P \subseteq f^{-1}(\{0\})$ , $Q \subseteq f^{-1}(\{1\})$ (Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0,1]$ , and conversely such a space is normal).

[L4]

Tychonoff means completely regular and $T_1$ (Completely regular spaces and Tychonoff ( $T_{3\frac{1}{2}}$ ) spaces, $T_0$ (Kolmogorov) and $T_1$ (Frechet) spaces).

Proof

technique · direct

1.1

$X$ is compact and Hausdorff (given); by [L1], $X$ is regular and normal, hence $T_3$ and $T_4$ , that is, in particular, normal and $T_1$ .

givenL1

2.1

By [L2] applied to step 1.1 (normal and $T_1$ ), $X$ is completely regular.

step 1.1L2

2.2

Let $A, B \subseteq X$ be disjoint closed sets; by [L3] applied to step 1.1 (normal), fix a continuous $f : X \to [0,1]$ with $A \subseteq f^{-1}(\{0\})$ and $B \subseteq f^{-1}(\{1\})$ .

step 1.1L3choose

3.1

By step 1.1 ( $T_1$ ) and step 2.1 (completely regular), $X$ is Tychonoff by [L4].

step 1.1step 2.1L4

4.1

Steps 3.1 and 2.2 establish the two clauses of the statement.

step 3.1step 2.2∎

Remarks

Nothing here is new mathematics. This item exists so that "compact Hausdorff" has a one-step citation to both Tychonoff-ness and to Urysohn separation, rather than requiring every citing page to chain A compact Hausdorff space is regular and normal, hence $T_3$ and $T_4$ through Under dependent choice a normal $T_1$ space is completely regular, so $T_4 \Rightarrow T_{3\frac{1}{2}}$ , and together with the implications already proved this is the whole classical chain or Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0,1]$ , and conversely such a space is normal by hand.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 116 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

Tychonoff space (Wikipedia) (standard reference, not scraped)
Compact space (Wikipedia) (standard reference, not scraped)
Urysohn's lemma (Wikipedia) (standard reference, not scraped)