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.

✓ 11 results · all verified · 8 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full by a delegated reviewing agent on the owner's instruction; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Urysohn's Lemma and the Tietze Extension Theorem

1 · Prerequisites

2 · Summary

Objective. Urysohn's lemma separates two disjoint closed sets of a normal space by a continuous real-valued function; Tietze's extension theorem extends a continuous function on a closed subspace of a normal space to the whole space. This page proves both, under the Axiom of Dependent Choice, and develops the mechanism each proof shares: a family of open sets indexed by the dyadic rationals of $[0, 1]$ , nested by closure, defines the separating or extending function as an infimum.

The mechanism. The dyadic rationals of $[0, 1]$ , their finite levels $D_{n}$ , and their density in $[0, 1]$ fixes the dyadic rationals of $[0, 1]$ level by level and proves their density. If $(U_{r})_{r \in D}$ are open with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ and $U_{1} = X$ , then $x \mapsto \inf {r \in D : x \in U_{r}}$ is a continuous map $X \to [0, 1]$ , and no choice principle is used shows, without any choice principle, that a family of open sets indexed by those dyadics with closures nested inside the next member defines a continuous map into $[0, 1]$ ; every choice-consuming step of the page happens earlier, in building such a family, never in this lemma.

Urysohn's lemma and its converse. 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 builds a nested dyadic family by dependent choice and proves that a normal space's disjoint closed sets are separated by a continuous function into $[0, 1]$ ; it also proves the converse, that a space with this separation property is normal, with no choice principle. 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 applies the lemma to a point and a closed set in a normal $T_{1}$ space, supplying the arrow $T_{4} \Rightarrow T_{3 \frac{1}{2}}$ and assembling it with the implications already proved elsewhere into the full classical separation chain.

Tietze's extension theorem. If for every $ε > 0$ some continuous $g : X \to R$ satisfies $∣ f (x) - g (x) ∣ < ε$ for all $x$ , then $f$ is continuous; in particular a uniformly convergent series of continuous real functions has a continuous sum proves that a real-valued function approximable to any tolerance by a continuous function is itself continuous, and in particular that a series of continuous functions dominated termwise by a convergent series of constants has a continuous sum. Under dependent choice a space is perfectly normal if and only if it is normal and every closed set is a zero set combines this with Urysohn's lemma to characterise perfect normality: a normal space is perfectly normal exactly when every closed set is the zero set of a continuous function. Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a, b]$ extends continuously to the whole space, and this property characterises normality combines it with a geometrically decaying series of Urysohn functions to extend a continuous map on a closed subspace into $[a, b]$ , and proves the converse: the extension property characterises normality. Under dependent choice, a continuous real-valued map on a closed subspace of a normal space extends to the whole space, and a map into an open interval extends into that same open interval widens the target from a closed bounded interval to $R$ and to an open interval, composing the bounded case with an explicit homeomorphism.

Compactness and complete regularity. Under dependent choice a locally compact Hausdorff space is completely regular, hence Tychonoff applies Urysohn's lemma inside the one-point compactification of a locally compact Hausdorff space to show it is completely regular, hence Tychonoff. Under dependent choice a compact Hausdorff space is Tychonoff, and its disjoint closed sets are separated by continuous functions records the compact Hausdorff case directly, together with Urysohn separation for its own disjoint closed sets.

Choice cost. Which results on this page spend dependent choice, which spend countable choice, and which are theorems of ZF accounts for where each theorem on this page spends dependent choice, where the perfect-normality theorem separately performs a step shaped like countable choice and discharges it as an instance of dependent choice, and which results — the dyadic-scale lemma, the $M$ -test, and the metric case of every theorem here — use no choice principle at all.

False statements mark the boundary of what normality alone supplies. FALSE: Every normal space is completely regular refutes normality without $T_{1}$ implying complete regularity, using Sierpinski space. FALSE: Every continuous real-valued function on a subspace of a normal space extends continuously to the whole space refutes the extension property for a subspace that is not closed, using the reciprocal function on $(0, 1]$ .

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

The dyadic rationals of $[0, 1]$ , their finite levels $D_{n}$ , and their density in $[0, 1]$

Definition

Throughout, $ι$ is the canonical natural of $R$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field), and as is standard $ι (k)$ is abbreviated to $k$ once no ambiguity results (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ). For $m, n \in N$ , $m^{n} \in N$ is the natural-number power of Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ , distinct from but agreeing with the real (integer) power $a^{n}$ of Integer powers $a^{m}$ by that item's clause (d): $ι (m^{n}) = ι (m)^{n}$ . Writing $2$ for $ι (2)$ as just agreed, this lets $2^{n}$ be read as a natural number or as the real $ι (2)^{n}$ interchangeably.

For $n \in N$ put

$D_{n} : = {\frac{k}{2^{n}} : k \in N, k \leq 2^{n}} \subseteq [0, 1],$

the order $\leq$ on the naturals $k$ and $2^{n}$ being that of Order on the natural numbers. Each $D_{n}$ is a finite subset of $[0, 1]$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) with $0, 1 \in D_{n}$ (the cases $k = 0$ and $k = 2^{n}$ ); it has at most $2^{n} + 1$ elements, so is finite in the sense of Finite, countably infinite, countable, uncountable. The dyadic rationals of $[0, 1]$ are

$D : = ⋃_{n \in N} D_{n} \subseteq [0, 1],$

a countable union of finite sets. Each level $D_{n}$ is nested in the next: if $k \leq 2^{n}$ then $2 k \leq 2^{n + 1}$ (multiplying the natural inequality by $2$ ), and $\frac{k}{2^{n}} = \frac{2 k}{2^{n + 1}}$ in $R$ (clearing the common factor $ι (2)$ , licensed by Ordered field), so every element of $D_{n}$ is exhibited as an element of $D_{n + 1}$ ; hence $D_{0} \subseteq D_{1} \subseteq D_{2} \subseteq \dots$ and $D = ⋃_{n} D_{n}$ is genuinely increasing, not merely a union.

The level decomposition, stated and discharged here because the recursion 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 consumes it. For $n \in N$ ,

$D_{n + 1} = D_{n} \cup {t_{j} : = \frac{2 j + 1}{2^{n + 1}} : j \in N, j < 2^{n}},$

and the new points $t_{j}$ are pairwise distinct, none lies in $D_{n}$ , and each lies strictly between the $D_{n}$ -consecutive pair $r_{j} : = j / 2^{n}$ and $s_{j} : = (j + 1) / 2^{n}$ . Strict betweenness: $2 j < 2 j + 1 < 2 j + 2$ , and dividing by the positive $2^{n + 1}$ preserves strict order (Ordered field), so $r_{j} = 2 j / 2^{n + 1} < t_{j} < (2 j + 2) / 2^{n + 1} = s_{j}$ . Distinctness: $j \mapsto 2 j + 1$ is injective. Disjointness from $D_{n}$ : $t_{j} = k / 2^{n}$ with $k \leq 2^{n}$ would give $2 j + 1 = 2 k$ after clearing the positive factor $1 / 2^{n + 1}$ and applying injectivity of $ι$ ; but $k \leq j$ gives $2 k \leq 2 j < 2 j + 1$ , and $k \geq j + 1$ gives $2 k \geq 2 j + 2 > 2 j + 1$ , so no such $k$ exists. The union is all of $D_{n + 1}$ : given $k / 2^{n + 1}$ with $k \leq 2^{n + 1}$ , the set ${i \in N : 2 i > k}$ is nonempty ( $2 (k + 1) = 2 k + 2 > k$ ), so by The well-ordering principle it has a least element $i_{0}$ , and $i_{0} \geq 1$ since $2 \cdot 0 = 0 \leq k$ ; writing $i_{0} = j + 1$ (Every nonzero natural number is a successor) gives $2 j \leq k < 2 j + 2$ , so $k = 2 j$ or $k = 2 j + 1$ . In the first case $k / 2^{n + 1} = j / 2^{n} \in D_{n}$ (with $j \leq 2^{n}$ since $2 j \leq 2^{n + 1}$ ); in the second it is $t_{j}$ (with $j < 2^{n}$ since $2 j + 1 \leq 2^{n + 1}$ forces $2 j < 2^{n + 1}$ ). Finally, any two elements of $D$ lie together in a common level: one lies in some $D_{m}$ and the other in some $D_{m^{'}}$ , and both then lie in $D_{\max (m, m^{'})}$ by the nesting just proved.

$D$ is dense in $[0, 1]$ : for every $x \in [0, 1]$ and every real $ε > 0$ there is $r \in D$ with $∣ x - r ∣ < ε$ . First, a growth fact about natural-number powers, proved by induction on $n$ (The principle of mathematical induction): $2^{n} \geq n + 1$ for every $n \in N$ . At $n = 0$ , $2^{0} = 1 = 0 + 1$ . If $2^{n} \geq n + 1$ , then $2^{n + 1} = 2^{n} \cdot 2 = 2^{n} + 2^{n} \geq (n + 1) + (n + 1) = 2 n + 2 \geq n + 2 = (n + 1) + 1$ , the middle inequality adding the inductive hypothesis to itself and the last holding since $n \geq 0$ ; both steps use only that the order of $N$ is compatible with addition (Order on the natural numbers). Transporting the inequality into $R$ by the order-preserving $ι$ (Canonical naturals are positive and strictly increasing) gives $ι (2^{n}) \geq ι (n + 1) = ι (n) + 1$ for every $n$ .

Now fix $x \in [0, 1]$ and a real $ε > 0$ . By For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ fix a natural $m \geq 1$ with $1 / m < ε$ . Put $n : = m$ ; then $ι (2^{n}) \geq ι (n) + 1 = ι (m) + 1 > ι (m) > 0$ , so by Inverses of positives are positive, and reciprocation reverses order $0 < 1 / 2^{n} < 1 / m < ε$ . Consider $S : = {k \in N : x \leq k / 2^{n}}$ . It is nonempty, since $k = 2^{n}$ satisfies $x \leq 1 = 2^{n} / 2^{n}$ because $x \in [0, 1]$ ; so by The well-ordering principle $S$ has a least element $k_{0}$ , and $k_{0} \leq 2^{n}$ because $2^{n} \in S$ . If $k_{0} = 0$ then $x \leq 0$ , and $x \geq 0$ since $x \in [0, 1]$ , so $x = 0 = 0 / 2^{n} \in D_{n} \subseteq D$ , within distance $0 < ε$ of itself. If $k_{0} \geq 1$ then $k_{0} - 1 \in N$ and, by minimality of $k_{0}$ , $k_{0} - 1 \notin S$ , that is $x > (k_{0} - 1) / 2^{n} = k_{0} / 2^{n} - 1 / 2^{n}$ ; combined with $x \leq k_{0} / 2^{n}$ this gives $∣ x - k_{0} / 2^{n} ∣ \leq 1 / 2^{n} < ε$ , and $r : = k_{0} / 2^{n} \in D_{n} \subseteq D$ since $k_{0} \leq 2^{n}$ . Either way some $r \in D$ satisfies $∣ x - r ∣ < ε$ .

Remarks

Every dyadic rational of $[0, 1]$ other than $0$ and $1$ lies strictly between them, since $0 < k / 2^{n} < 1$ exactly when $0 < k < 2^{n}$ .
The finite levels, not $D$ itself, are what the construction of Urysohn's lemma recurses on. $D$ is presented here as the increasing union $⋃_{n} D_{n}$ precisely so that a family indexed by $D$ can be built one finite level at a time, each level adding only finitely many new indices to the one before.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

If $(U_{r})_{r \in D}$ are open with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ and $U_{1} = X$ , then $x \mapsto \inf {r \in D : x \in U_{r}}$ is a continuous map $X \to [0, 1]$ , and no choice principle is used

Statement

Let $(X, T)$ be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) and let $D$ be the dyadic rationals of $[0, 1]$ (The dyadic rationals of $[0, 1]$ , their finite levels $D_{n}$ , and their density in $[0, 1]$ ). Let $(U_{r})_{r \in D}$ be a family of open subsets of $X$ such that

$\overline{U_{r}} \subseteq U_{s} whenever r < s in D, and U_{1} = X .$

Then

$f (x) : = \inf ({r \in D : x \in U_{r}} \cup {1})$

defines a map $f : X \to [0, 1]$ , and $f$ is continuous.

No choice principle is used in passing from the family $(U_{r})_{r \in D}$ to $f$ . Every existential instantiation in the proof below is a single choice from a single nonempty set of reals, never a simultaneous selection over an infinite index; where the family $(U_{r})_{r \in D}$ itself is later built by a choice-consuming recursion, that cost is incurred in producing the family, not in this lemma.

Facts & Assumptions

Given: A topological space $(X, T)$ , the dyadic rationals $D$ of $[0, 1]$ , and a family $(U_{r})_{r \in D}$ of open subsets of $X$ with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ in $D$ , and $U_{1} = X$ .

[A1]

Shrinking hypothesis: for $r < s$ in $D$ , $\overline{U_{r}} \subseteq U_{s}$ .

[A2]

$U_{1} = X$ .

[L1]

$D \subseteq [0, 1]$ , and $D$ is dense in $[0, 1]$ : for every $x \in [0, 1]$ and every real $ε > 0$ there is $r \in D$ with $∣ x - r ∣ < ε$ (The dyadic rationals of $[0, 1]$ , their finite levels $D_{n}$ , and their density in $[0, 1]$ ).

[L2]

Infimum: a nonempty $S \subseteq R$ bounded below has $\inf S \in R$ (Every nonempty set bounded below has an infimum), which is a lower bound of $S$ and is $\geq$ every other lower bound of $S$ (Greatest lower bound (infimum)). Consequently, for a real $a$ : (i) if some $s \in S$ has $s < a$ then $\inf S \leq s < a$ ; (ii) if $\inf S < a$ then some $s \in S$ has $s < a$ , since otherwise $a$ would be a lower bound of $S$ forcing $a \leq \inf S$ ; (iii) if $r < \inf S$ then $r < s$ for every $s \in S$ , since $\inf S$ is itself a lower bound of $S$ .

[L3]

The traces on $[0, 1]$ of the order rays, $[0, a) : = (- \infty, a) \cap [0, 1]$ and $(a, 1] : = (a, \infty) \cap [0, 1]$ for $a \in R$ , form a subbasis for the subspace topology of $[0, 1]$ (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). Indeed each ray $(- \infty, a)$ , $(a, \infty)$ is a union of bounded open intervals of $R$ , hence open in the usual topology (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not), so the topology the rays generate is contained in the usual topology of $R$ ; and every bounded open interval $(a, b)$ is the intersection $(a, \infty) \cap (- \infty, b)$ of two rays, so by A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis the finite intersections of the rays already form a basis containing every bounded open interval, hence the rays generate at least the usual topology. The two inclusions make the rays a subbasis for the usual topology of $R$ (Basis and subbasis for a topology, and the topology generated by a family of sets), and tracing a subbasis onto a subspace gives a subbasis for the subspace topology (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).

[L4]

Checking preimages of a fixed subbasis suffices for continuity (For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ , clause (d) $\Leftrightarrow$ (a)).

[L5]

$A \subseteq \overline{A}$ for every $A \subseteq X$ , and $X ∖ \overline{A}$ is open (Interior, closure, boundary, exterior, derived set and isolated point in a topological space, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Proof

technique · direct

1.1

For $x \in X$ put $S_{x} : = {r \in D : x \in U_{r}} \cup {1}$ ; then $S_{x}$ is a nonempty subset of $[0, 1]$ , since $1 \in S_{x}$ and $D \subseteq [0, 1]$ by [L1], so $S_{x}$ is bounded below by $0$ and above by $1$ .

givenL1

2.1

By step 1.1 and [L2], $\inf S_{x}$ exists in $R$ for every $x \in X$ , lies in $[0, 1]$ since $0$ is a lower bound of $S_{x}$ and $\inf S_{x} \leq 1$ as $1 \in S_{x}$ ; define $f : X \to [0, 1]$ by $f (x) : = \inf S_{x}$ .

step 1.1L2construct

3.1

For every $x \in X$ and real $a$ with $0 < a \leq 1$ : if there is $r \in D$ with $r < a$ and $x \in U_{r}$ , then $r \in S_{x}$ , so $f (x) \leq r < a$ by L2.

step 2.1L2

3.2

For every $x \in X$ and real $a$ with $0 < a \leq 1$ : if $f (x) < a$ , then by L2 some $s \in S_{x}$ has $s < a \leq 1$ , so $s \neq 1$ , hence $s \in D$ and $x \in U_{s}$ , with $s < a$ .

step 2.1L2

3.3

For real $a \leq 0$ : ${x : f (x) < a} = \emptyset$ , since $f (x) \geq 0$ always by step 2.1; for real $a > 1$ : ${x : f (x) < a} = X$ , since $f (x) \leq 1 < a$ always by step 2.1; both open.

step 2.1

3.4

For every $x \in X$ and real $a$ with $0 \leq a < 1$ : if $f (x) > a$ , put $x_{0} : = (a + f (x)) / 2 \in (a, f (x)) \subseteq [0, 1]$ and $δ : = (f (x) - a) / 2 > 0$ ; by [L1] fix $r_{1} \in D$ with $∣ x_{0} - r_{1} ∣ < δ$ , so $r_{1} \in (a, f (x))$ .

step 2.1L1choose

3.5

For every $x \in X$ , real $a$ with $0 \leq a < 1$ , and $r \in D$ with $r > a$ : if $x \notin \overline{U_{r}}$ , then $r$ is a lower bound of $S_{x}$ . Indeed, for $s = 1 \in S_{x}$ : $r \leq 1 = s$ , since $r \in D \subseteq [0, 1]$ by [L1]; for $s \in D$ with $x \in U_{s}$ : if $s < r$ then [A1] gives $\overline{U_{s}} \subseteq U_{r}$ , so $x \in U_{s} \subseteq \overline{U_{s}} \subseteq U_{r} \subseteq \overline{U_{r}}$ by [L5], contradicting $x \notin \overline{U_{r}}$ , so $s \geq r$ .

step 2.1A1L1L5

3.6

For real $a < 0$ : ${x : f (x) > a} = X$ , since $f (x) \geq 0 > a$ always by step 2.1; for real $a \geq 1$ : ${x : f (x) > a} = \emptyset$ , since $f (x) \leq 1 \leq a$ always.

step 2.1

4.1

For real $a$ with $0 < a \leq 1$ : ${x \in X : f (x) < a} = ⋃_{r \in D, r < a} U_{r}$ , by steps 3.1 and 3.2 giving the two inclusions; a union of open sets, hence open.

step 3.1step 3.2

4.2

Continuing under the hypothesis of step 3.4: since $a < r_{1}$ , by [L1] fix $r_{2} \in D$ with $∣ (a + r_{1}) / 2 - r_{2} ∣ < (r_{1} - a) / 2$ , so $r_{2} \in (a, r_{1})$ .

step 3.4L1choose

4.3

Continuing under the hypothesis of step 3.5: since $r$ is a lower bound of $S_{x}$ by step 3.5, [L2] gives $r \leq \inf S_{x} = f (x)$ ; combined with $r > a$ , $f (x) > a$ .

step 3.5step 2.1L2

5.1

Continuing, with $r_{1}, r_{2}$ as in step 4.2: since $r_{1} < f (x) = \inf S_{x}$ , L2 gives $r_{1} < s$ for every $s \in S_{x}$ ; in particular $r_{1} \neq 1$ , since $r_{1} < f (x) \leq 1$ , so $r_{1} \notin S_{x}$ forces $x \notin U_{r_{1}}$ , as otherwise $r_{1}$ itself would lie in $S_{x}$ .

step 3.4step 2.1L2

6.1

Continuing: since $r_{2} < r_{1}$ in $D$ , [A1] gives $\overline{U_{r_{2}}} \subseteq U_{r_{1}}$ ; if $x \in \overline{U_{r_{2}}}$ then $x \in U_{r_{1}}$ , contradicting step 5.1; so $x \notin \overline{U_{r_{2}}}$ , and $r_{2} > a$ .

step 4.2step 5.1A1

7.1

For real $a$ with $0 \leq a < 1$ : ${x \in X : f (x) > a} = ⋃_{r \in D, r > a} (X ∖ \overline{U_{r}})$ . A point of the left side has, by steps 3.4 and 6.1, some $r = r_{2} \in D$ with $r > a$ and $x \in X ∖ \overline{U_{r}}$ ; a point $x$ of the right side lies in $X ∖ \overline{U_{r}}$ for some such $r$ , hence $x \notin \overline{U_{r}}$ , giving $f (x) > a$ by step 4.3. Each $X ∖ \overline{U_{r}}$ is open by [L5], so the union is open.

step 6.1step 4.3L5

8.1

By [L3], the sets $[0, a)$ and $(a, 1]$ , $a \in R$ , form a subbasis for the subspace topology of $[0, 1]$ ; and $f^{- 1} ([0, a)) = {x : f (x) < a}$ , $f^{- 1} ((a, 1]) = {x : f (x) > a}$ are open in $X$ for every real $a$ , by steps 4.1, 3.3, 7.1 and 3.6.

step 4.1step 3.3step 7.1step 3.6L3

9.1

By [L4], since the preimage of every member of that subbasis is open, $f$ is continuous as a map $X \to [0, 1]$ ; together with step 2.1 this proves the statement.

step 8.1step 2.1L4∎

Remarks

Why the $\cup {1}$ in the definition of $f$ . It is what makes $S_{x}$ manifestly nonempty and bounded above by $1$ without first invoking $U_{1} = X$ ; under that hypothesis $1 \in D$ already forces $1 \in S_{x}$ on its own (since every $x \in X = U_{1}$ ), so the union is not strictly necessary here, but it keeps well-definedness visible from the definition of $S_{x}$ alone, which matters when this lemma is quoted with a family for which the reader has not yet checked $U_{1} = X$ line by line.
Where density of $D$ is spent, and only there. The forward half of the " $f (x) > a$ " characterisation (steps 3.4, 4.2, 5.1 and 6.1) is the only place two dyadic points strictly between $a$ and $f (x)$ are extracted; the " $f (x) < a$ " half needs no density at all, only the defining property of an infimum. This asymmetry mirrors the asymmetry of the hypothesis: the shrinking clause $\overline{U_{r}} \subseteq U_{s}$ supplies a closed set inside an open one, and closing the resulting gap is what the second dyadic point is for.
The subbasis fact (Fact [L3]) has no home elsewhere in this library at this point in the reading order: no earlier item states that the order rays generate the usual topology of $R$ , so it is derived here from the basis criterion rather than cited as a single fact.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)‡ rests on unproved materialOpen item page →

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

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). Let $(X, T)$ be a topological space.

If $X$ is normal (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly) and $A, B \subseteq X$ are disjoint closed sets, there is a continuous $f : X \to [0, 1]$ (Continuity of a map of topological spaces at a point and globally, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) with $A \subseteq f^{- 1} ({0})$ and $B \subseteq f^{- 1} ({1})$ .
Conversely, if every pair of disjoint closed subsets of $X$ admits a continuous function into $[0, 1]$ separating them in the sense of clause 1, then $X$ is normal. This direction uses no choice principle.

Where the choice principle of clause 1 is spent, and why not less. The construction below builds, for each $n \in N$ , an assignment of an open set to every dyadic rational of level $n$ , extending the level- $(n - 1)$ assignment; at each single level the finitely many new open sets are chosen at once by Every natural-number-indexed list of nonempty sets has a choice function on its family of values, a theorem of ZF, but stringing together infinitely many such levels, each depending on the one before, is exactly the situation dependent choice is for. The published Urysohn's lemma is not a theorem of ZF, nor of ZF plus countable choice ‡ records, with its sources, that $Z F$ and even $Z F$ together with the Axiom of Countable Choice do not suffice, and that dependent choice does; nothing here claims dependent choice is necessary for clause 1, only that the construction given is carried out in $Z F + D C$ .

Facts & Assumptions

Given: A topological space $(X, T)$ and dependent choice.

[A1]

$D C$ : for every nonempty set $P$ , every relation $R \subseteq P \times P$ entire on $P$ (every $p \in P$ has some $q \in P$ with $p R q$ ), and every $a \in P$ , there is a sequence $(p_{k})_{k \in N}$ with $p_{0} = a$ and $p_{k} R p_{k + 1}$ for every $k$ (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[L1]

Shrinking: if $X$ is normal, $C \subseteq X$ is closed and $O \subseteq X$ is open with $C \subseteq O$ , then there is open $W$ with $C \subseteq W \subseteq \overline{W} \subseteq O$ (A space is normal if and only if every closed $A$ inside an open $U$ admits an open $V$ with $A \subseteq V \subseteq \overline{V} \subseteq U$ ).

[L2]

Finite choice: a function $F$ with domain a natural number $n$ , all of whose values are nonempty sets, admits a choice function for the family $F [n]$ of its values (Every natural-number-indexed list of nonempty sets has a choice function on its family of values, Choice function), a theorem of ZF.

[L3]

The dyadic rationals $D = ⋃_{n} D_{n}$ of $[0, 1]$ are an increasing union of finite levels; for $n \in N$ , $D_{n + 1} = D_{n} \cup {t_{j} : 0 \leq j < 2^{n}}$ , where $t_{j}$ is strictly between the $D_{n}$ -consecutive pair $r_{j} : = j / 2^{n}$ and $s_{j} : = (j + 1) / 2^{n}$ , the $2^{n}$ points $t_{j}$ are pairwise distinct and disjoint from $D_{n}$ , and every two elements of $D$ lie together in some common $D_{n}$ (The dyadic rationals of $[0, 1]$ , their finite levels $D_{n}$ , and their density in $[0, 1]$ ).

[L4]

Chaining: if $V_{0}, \dots, V_{k}$ ( $k \geq 0$ ) are subsets of $X$ with $\overline{V_{i}} \subseteq V_{i + 1}$ for every $i < k$ , then $\overline{V_{0}} \subseteq V_{k}$ , since $V_{i} \subseteq \overline{V_{i}} \subseteq V_{i + 1}$ for each $i$ (Interior, closure, boundary, exterior, derived set and isolated point in a topological space) makes $\overline{V_{0}} \subseteq V_{1} \subseteq V_{2} \subseteq \dots \subseteq V_{k}$ a chain of inclusions.

[L5]

The generic construction: if $(U_{r})_{r \in D}$ is a family of open subsets of $X$ with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ in $D$ and $U_{1} = X$ , then $g (x) : = \inf ({r \in D : x \in U_{r}} \cup {1})$ is a continuous map $X \to [0, 1]$ (If $(U_{r})_{r \in D}$ are open with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ and $U_{1} = X$ , then $x \mapsto \inf {r \in D : x \in U_{r}}$ is a continuous map $X \to [0, 1]$ , and no choice principle is used).

[L6]

The order rays $(- \infty, \frac{1}{2})$ and $(\frac{1}{2}, \infty)$ are open in the usual topology of $R$ (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, clause 3), so their traces $[0, \frac{1}{2})$ and $(\frac{1}{2}, 1]$ are open in the subspace topology of $[0, 1]$ (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$ : the nine order-convex forms, nondegeneracy, and length). They are disjoint and contain $0$ and $1$ , respectively.

[L7]

Preimages of open sets under a continuous map are open (For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ , clause (b), Continuity of a map of topological spaces at a point and globally).

[L8]

$A \subseteq \overline{A}$ for every $A \subseteq X$ (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

Proof

technique · constructive

1.1

Assume $X$ is normal and $A, B \subseteq X$ are disjoint closed sets (the hypothesis of clause 1).

assume-hyp

1.2

Assume instead that every pair of disjoint closed subsets of $X$ admits a continuous function into $[0, 1]$ separating them as in clause 1 (the hypothesis of clause 2).

assume-hyp

2.1

Under step 1.1: $A \subseteq X ∖ B$ , since $A \cap B = \emptyset$ , and $X ∖ B$ is open since $B$ is closed; by [L1] applied to the closed set $A$ and the open set $X ∖ B$ , fix open $Φ_{0} (0)$ with $A \subseteq Φ_{0} (0) \subseteq \overline{Φ_{0} (0)} \subseteq X ∖ B$ , and put $Φ_{0} (1) : = X ∖ B$ , defining $Φ_{0} : D_{0} \to T$ on $D_{0} = {0, 1}$ .

step 1.1L1chooseconstruct

2.2

Under step 1.2: let $C, E \subseteq X$ be disjoint closed sets; fix a continuous $h : X \to [0, 1]$ with $C \subseteq h^{- 1} ({0})$ and $E \subseteq h^{- 1} ({1})$ .

step 1.2choose

3.1

Under step 1.1: $A \subseteq Φ_{0} (0)$ ; $\overline{Φ_{0} (0)} \subseteq Φ_{0} (1)$ ; and $Φ_{0} (1) = X ∖ B$ .

step 2.1

3.2

Under step 1.2, continuing: by [L6], $[0, \frac{1}{2})$ and $(\frac{1}{2}, 1]$ are open in $[0, 1]$ , disjoint, with $0 \in [0, \frac{1}{2})$ and $1 \in (\frac{1}{2}, 1]$ ; put $O_{1} : = h^{- 1} ([0, \frac{1}{2}))$ and $O_{2} : = h^{- 1} ((\frac{1}{2}, 1])$ , open in $X$ by [L7].

step 2.2L6L7

4.1

Under step 1.1: for $n \in N$ , call $Φ : D_{n} \to T$ admissible at level $n$ when (i) $\overline{Φ (r)} \subseteq Φ (s)$ for every $r < s$ in $D_{n}$ ; (ii) $A \subseteq Φ (0)$ ; (iii) $Φ (1) = X ∖ B$ . Put $P : = {(n, Φ) : n \in N, Φ admissible at level n}$ , and for $(n, Φ), (n^{'}, Φ^{'}) \in P$ say $(n, Φ) R (n^{'}, Φ^{'})$ when $n^{'} = n + 1$ and $Φ^{'} ∣_{D_{n}} = Φ$ . By step 3.1, $(0, Φ_{0}) \in P$ .

step 3.1construct

4.2

Under step 1.2: $C \subseteq O_{1}$ , since $h \equiv 0 \in [0, \frac{1}{2})$ on $C$ ; $E \subseteq O_{2}$ , since $h \equiv 1 \in (\frac{1}{2}, 1]$ on $E$ ; and $O_{1} \cap O_{2} = h^{- 1} ([0, \frac{1}{2}) \cap (\frac{1}{2}, 1]) = h^{- 1} (\emptyset) = \emptyset$ .

step 2.2step 3.2L6

5.1

Under step 1.1: let $(n, Φ) \in P$ . For each $j$ with $0 \leq j < 2^{n}$ , with $r_{j}, s_{j}, t_{j}$ as in [L3]: since $r_{j} < s_{j}$ in $D_{n}$ , admissibility (i) gives $\overline{Φ (r_{j})} \subseteq Φ (s_{j})$ , so by [L1] the set of open $W$ with $\overline{Φ (r_{j})} \subseteq W \subseteq \overline{W} \subseteq Φ (s_{j})$ is nonempty.

step 4.1L1L3

5.2

Under step 1.2: since $C, E$ were an arbitrary disjoint closed pair, step 4.2 exhibits disjoint open supersets for every such pair, so $X$ is normal by Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly; this is clause 2, and no step of it used [A1].

step 4.2

6.1

Under step 1.1, continuing under step 5.1: by [L2] applied to the function assigning, to each $j < 2^{n}$ , the nonempty set of open $W$ with $\overline{Φ (r_{j})} \subseteq W \subseteq \overline{W} \subseteq Φ (s_{j})$ , fix a simultaneous choice, giving open $W_{j}$ with $\overline{Φ (r_{j})} \subseteq W_{j} \subseteq \overline{W_{j}} \subseteq Φ (s_{j})$ for every $0 \leq j < 2^{n}$ .

step 5.1L2choose

7.1

Under step 1.1: define $Φ^{'} : D_{n + 1} \to T$ by $Φ^{'} ∣_{D_{n}} : = Φ$ and $Φ^{'} (t_{j}) : = W_{j}$ for $0 \leq j < 2^{n}$ ; this is well defined since $D_{n + 1} = D_{n} \cup {t_{j} : 0 \leq j < 2^{n}}$ with the $t_{j}$ pairwise distinct and disjoint from $D_{n}$ by [L3]. Then $(n, Φ) R (n + 1, Φ^{'})$ .

step 6.1L3construct

8.1

Under step 1.1, with $Φ, Φ^{'}$ as in step 7.1: for the $D_{n + 1}$ -consecutive pair $(r_{j}, t_{j})$ : $\overline{Φ^{'} (r_{j})} = \overline{Φ (r_{j})} \subseteq W_{j} = Φ^{'} (t_{j})$ by step 6.1; for the pair $(t_{j}, s_{j})$ : $\overline{Φ^{'} (t_{j})} = \overline{W_{j}} \subseteq Φ (s_{j}) = Φ^{'} (s_{j})$ by step 6.1.

step 7.1step 6.1

9.1

Under step 1.1: for $x < y$ in $D_{n + 1}$ , the finitely many elements of $D_{n + 1} \cap [x, y]$ , listed increasingly as $x = u_{0} < u_{1} < \dots < u_{k} = y$ , are $D_{n + 1}$ -consecutive at each step $u_{i} < u_{i + 1}$ , and each such pair is one of the pairs of step 8.1 (every $D_{n + 1}$ -consecutive pair has at least one member among the new points $t_{j}$ , since a new point was inserted into every $D_{n}$ -consecutive gap); so $\overline{Φ^{'} (u_{i})} \subseteq Φ^{'} (u_{i + 1})$ at each step, and [L4] gives $\overline{Φ^{'} (x)} = \overline{Φ^{'} (u_{0})} \subseteq Φ^{'} (u_{k}) = Φ^{'} (y)$ .

step 8.1L3L4

10.1

Under step 1.1: $A \subseteq Φ^{'} (0) = Φ (0)$ , since $0 \in D_{n}$ is unaffected by the extension; $Φ^{'} (1) = Φ (1) = X ∖ B$ , since $1 \in D_{n}$ is likewise unaffected; with step 9.1 this is admissibility of $Φ^{'}$ at level $n + 1$ , so $(n + 1, Φ^{'}) \in P$ .

step 7.1step 9.1L3

11.1

Under step 1.1: by steps 5.1, 6.1, 7.1 and 10.1, every $(n, Φ) \in P$ has some $(n + 1, Φ^{'}) \in P$ with $(n, Φ) R (n + 1, Φ^{'})$ ; so $R$ is entire on $P$ .

step 7.1step 10.1

12.1

Under step 1.1: $P$ is nonempty by step 4.1 and $R$ is entire on $P$ by step 11.1; by [A1] applied with $a : = (0, Φ_{0})$ , there is a sequence $((m_{k}, Ψ_{k}))_{k \in N}$ with $(m_{0}, Ψ_{0}) = (0, Φ_{0})$ and $(m_{k}, Ψ_{k}) R (m_{k + 1}, Ψ_{k + 1})$ for every $k$ .

step 4.1step 11.1A1construct

13.1

Under step 1.1: since $(n, Φ) R (n^{'}, Φ^{'})$ forces $n^{'} = n + 1$ , and $m_{0} = 0$ , induction on $k$ gives $m_{k} = k$ for every $k \in N$ ; so each $Ψ_{k} : D_{k} \to T$ is admissible at level $k$ , and $Ψ_{k + 1} ∣_{D_{k}} = Ψ_{k}$ for every $k$ .

step 12.1

14.1

Under step 1.1: for $r \in D$ , fix $n$ with $r \in D_{n}$ [L3] and define $V_{r} : = Ψ_{n} (r)$ ; by step 13.1, for $n \leq n^{'}$ with $r \in D_{n}$ , $Ψ_{n^{'}} (r) = Ψ_{n} (r)$ (chaining $Ψ_{n^{'}} ∣_{D_{n}} = Ψ_{n}$ through the intermediate levels), so $V_{r}$ does not depend on the level $n$ chosen.

step 13.1L3construct

15.1

Under step 1.1: for $r < s$ in $D$ , fix $n$ with $r, s \in D_{n}$ [L3]; then $\overline{V_{r}} = \overline{Ψ_{n} (r)} \subseteq Ψ_{n} (s) = V_{s}$ by admissibility (i) of $Ψ_{n}$ . Also $A \subseteq V_{0}$ and $V_{1} = X ∖ B$ , by admissibility (ii) and (iii) of $Ψ_{n}$ for any $n$ .

step 14.1step 13.1L3

16.1

Under step 1.1: define $U_{r} : = V_{r}$ for $r \in D$ with $r < 1$ , and $U_{1} : = X$ . For $r < s$ in $D$ : if $s < 1$ , $\overline{U_{r}} = \overline{V_{r}} \subseteq V_{s} = U_{s}$ by step 15.1; if $s = 1$ , $\overline{U_{r}} = \overline{V_{r}} \subseteq V_{1} = X ∖ B \subseteq X = U_{1}$ by step 15.1. So $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ in $D$ , and $U_{1} = X$ .

step 15.1construct

17.1

Under step 1.1: by [L5] applied to $(U_{r})_{r \in D}$ of step 16.1, $f (x) : = \inf ({r \in D : x \in U_{r}} \cup {1})$ is a continuous map $X \to [0, 1]$ .

step 16.1L5

17.2

Under step 1.1: for $b \in B$ and $r \in D$ with $r < 1$ : fix $n$ with $r \in D_{n}$ [L3]; since $1 \in D_{n}$ also, admissibility (i) of $Ψ_{n}$ applied to $r < 1$ gives $\overline{Ψ_{n} (r)} \subseteq Ψ_{n} (1) = X ∖ B$ , that is $\overline{V_{r}} \subseteq X ∖ B$ ; since $V_{r} \subseteq \overline{V_{r}}$ by [L8] and $U_{r} = V_{r}$ by step 16.1, $U_{r} \cap B = \emptyset$ , so $b \notin U_{r}$ .

step 14.1step 13.1step 16.1L3L8

18.1

Under step 1.1: for $a \in A$ : $a \in V_{0}$ by step 15.1, and $U_{0} = V_{0}$ by step 16.1 (as $0 < 1$ ), so $a \in U_{0}$ and $0 \in {r \in D : a \in U_{r}}$ ; hence $f (a) \leq 0$ , and $f (a) \geq 0$ since $f$ maps into $[0, 1]$ by step 17.1, so $f (a) = 0$ .

step 17.1step 16.1step 15.1

18.2

Under step 1.1: for $b \in B$ : by step 17.2, $b \notin U_{r}$ for every $r \in D$ with $r < 1$ , and $b \in U_{1} = X$ by step 16.1; so ${r \in D : b \in U_{r}} \cup {1} = {1}$ , giving $f (b) = \inf {1} = 1$ .

step 17.2step 16.1

19.1

Steps 17.1, 18.1 and 18.2 show that, under the hypothesis of step 1.1, $f$ is a continuous map $X \to [0, 1]$ with $A \subseteq f^{- 1} ({0})$ and $B \subseteq f^{- 1} ({1})$ , which is clause 1.

step 17.1step 18.1step 18.2

20.1

Steps 19.1 and 5.2 establish clauses 1 and 2 respectively.

step 19.1step 5.2discharge-construct∎

Remarks

The lemma is stated for a normal space, not a $T_{4}$ space. $T_{1}$ is used nowhere above; it is needed only to turn a point into a closed set, which is the extra step the next corollary spends. The published Urysohn's lemma is not a theorem of ZF, nor of ZF plus countable choice ‡ states the classical $T_{4}$ form; the form proved here is the more general one, and the two are not in tension — the $T_{4}$ form follows by adding the $T_{1}$ hypothesis, which is not used in this proof at all.
Only clause 1 costs a choice principle, and it is spent at exactly one place: the single application of dependent choice in step 12.1, which strings together the countably many admissible levels built one finite step at a time in steps 5.1–10.1. Every other existential instantiation above (steps 2.1, 2.2 and 6.1) draws from a single nonempty set or, in step 6.1, from a finite family of them via Every natural-number-indexed list of nonempty sets has a choice function on its family of values, and neither costs anything beyond ZF.
Why the construction tracks $X ∖ B$ rather than $X$ at $r = 1$ . Recording $Φ_{n} (1) : = X ∖ B$ throughout the recursion, rather than $X$ , is what makes admissibility clause (i) alone carry the whole $B$ -avoidance property: since $1 \in D_{n}$ for every $n$ , clause (i) applied to any $r < 1$ already gives $\overline{Φ_{n} (r)} \subseteq Φ_{n} (1) = X ∖ B$ , with no separate bookkeeping. Only at the very end, in step 16.1, is the top value widened from $X ∖ B$ to $X$ , which is exactly what If $(U_{r})_{r \in D}$ are open with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ and $U_{1} = X$ , then $x \mapsto \inf {r \in D : x \in U_{r}}$ is a continuous map $X \to [0, 1]$ , and no choice principle is used requires.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

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

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). If $(X, T)$ is normal and $T_{1}$ , that is $T_{4}$ (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 completely regular (Completely regular spaces and Tychonoff ( $T_{3 \frac{1}{2}}$ ) spaces). Since $X$ is also $T_{1}$ , $X$ is Tychonoff, and $T_{4} \Rightarrow T_{3 \frac{1}{2}}$ .

Combined with The implications proved on this page: perfectly normal gives completely normal under countable choice, and completely normal gives normal; normal with $T_{1}$ gives $T_{3}$ ; completely regular gives regular; regular with $T_{1}$ gives Urysohn, hence Hausdorff, hence $T_{1}$ , hence $T_{0}$ ; and metrizable gives every one of them, every arrow of

$T_{6} \Rightarrow T_{5} \Rightarrow T_{4} \Rightarrow T_{3 \frac{1}{2}} \Rightarrow T_{3} \Rightarrow T_{2 \frac{1}{2}} \Rightarrow T_{2} \Rightarrow T_{1} \Rightarrow T_{0}$

now holds: the first arrow under the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), the arrow $T_{4} \Rightarrow T_{3 \frac{1}{2}}$ proved here under dependent choice, and every other arrow with no choice principle at all. No arrow of this chain is asserted to reverse.

Facts & Assumptions

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

[A1]

$X$ is normal (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly) and $T_{1}$ ( $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces).

[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]

Urysohn's lemma, clause 1: assuming DC, if $X$ is normal and $P, Q \subseteq X$ are disjoint closed sets, there is a continuous $h : X \to [0, 1]$ with $P \subseteq h^{- 1} ({0})$ and $Q \subseteq h^{- 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).

[L3]

$X$ is completely regular when for every closed $C$ and every $x_{0} \in X ∖ C$ there is a continuous $f : X \to [0, 1]$ with $f (x_{0}) = 1$ and $f \equiv 0$ on $C$ (Completely regular spaces and Tychonoff ( $T_{3 \frac{1}{2}}$ ) spaces).

[L4]

Clauses 3 and 4 of The implications proved on this page: perfectly normal gives completely normal under countable choice, and completely normal gives normal; normal with $T_{1}$ gives $T_{3}$ ; completely regular gives regular; regular with $T_{1}$ gives Urysohn, hence Hausdorff, hence $T_{1}$ , hence $T_{0}$ ; and metrizable gives every one of them: normal with $T_{1}$ implies $T_{3}$ ; completely regular implies regular, and Tychonoff implies $T_{3}$ ; and clauses 1, 2 and 5 give the remaining arrows of the displayed chain, clause 1 — perfectly normal implies completely normal, that is $T_{6} \Rightarrow T_{5}$ — under the Axiom of Countable Choice.

Proof

technique · direct

1.1

${x_{0}}$ is closed, since $X$ is $T_{1}$ by [A1].

A1L1

1.2

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

given

2.1

By [A1] $X$ is normal, so [L2] applies to the disjoint closed sets $C$ and ${x_{0}}$ : there is a continuous $f : X \to [0, 1]$ with $C \subseteq f^{- 1} ({0})$ and ${x_{0}} \subseteq f^{- 1} ({1})$ , that is $f \equiv 0$ on $C$ and $f (x_{0}) = 1$ .

step 1.1step 1.2A1L2

3.1

Since $C$ and $x_{0} \notin C$ were arbitrary, step 2.1 exhibits, for every closed $C$ and every $x_{0} \in X ∖ C$ , a continuous $f : X \to [0, 1]$ with $f (x_{0}) = 1$ and $f \equiv 0$ on $C$ ; by [L3] this makes $X$ completely regular.

step 2.1L3

4.1

Since $X$ is also $T_{1}$ by [A1], $X$ is Tychonoff, so $T_{4} \Rightarrow T_{3 \frac{1}{2}}$ .

step 3.1A1

5.1

By [L4], $T_{3 \frac{1}{2}} \Rightarrow T_{3} \Rightarrow T_{2 \frac{1}{2}} \Rightarrow T_{2} \Rightarrow T_{1} \Rightarrow T_{0}$ and $T_{6} \Rightarrow T_{5} \Rightarrow T_{4}$ all hold, the arrow $T_{6} \Rightarrow T_{5}$ under countable choice; combined with step 4.1, every arrow of the displayed chain holds.

step 4.1L4∎

Remarks

This corollary supplies exactly the one arrow the published separation-axioms page could not reach. That page's own rem-separation-axiom-conventions names the missing arrow as normal $T_{1}$ implies completely regular and records that no rearrangement of material already on that page could supply it, since the implication is Urysohn's lemma. Nothing in this corollary revisits or amends that page; it only supplies, at a later point in the reading order, the theorem that page named as absent.
The chain above is not asserted to be a theorem of ZF. Its weakest link is this corollary's own dependent-choice hypothesis, and the first arrow separately costs countable choice; neither cost is removed by combining the arrows, and no clause of The implications proved on this page: perfectly normal gives completely normal under countable choice, and completely normal gives normal; normal with $T_{1}$ gives $T_{3}$ ; completely regular gives regular; regular with $T_{1}$ gives Urysohn, hence Hausdorff, hence $T_{1}$ , hence $T_{0}$ ; and metrizable gives every one of them is reproved here.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

If for every $ε > 0$ some continuous $g : X \to R$ satisfies $∣ f (x) - g (x) ∣ < ε$ for all $x$ , then $f$ is continuous; in particular a uniformly convergent series of continuous real functions has a continuous sum

Statement

Let $(X, T)$ be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) and let $f : X \to R$ . If for every real $ε > 0$ there is a continuous $g_{ε} : X \to R$ (Continuity of a map of topological spaces at a point and globally) with

$∣ f (x) - g_{ε} (x) ∣ < ε for every x \in X,$

then $f$ is continuous.

In particular, if $(g_{n})_{n \in N}$ are continuous real-valued functions on $X$ and $(M_{n})_{n \in N}$ are nonnegative reals with $∣ g_{n} (x) ∣ \leq M_{n}$ for every $x \in X$ and every $n$ , and the series $\sum M_{n}$ converges (Series, partial sums, convergence and the sum, divergence, and the tail series), then for every $x \in X$ the series $\sum g_{n} (x)$ converges, and

$F (x) : = \sum_{n = 0}^{\infty} g_{n} (x)$

defines a continuous function $F$ on $X$ .

Facts & Assumptions

Given: A topological space $(X, T)$ and $f : X \to R$ such that for every real $ε > 0$ there is a continuous $g_{ε} : X \to R$ with $∣ f (x) - g_{ε} (x) ∣ < ε$ for every $x \in X$ ; and, for the second clause, continuous $g_{n} : X \to R$ and nonnegative reals $M_{n}$ , $n \in N$ , with $∣ g_{n} (x) ∣ \leq M_{n}$ for every $x \in X, n \in N$ , and $\sum M_{n}$ convergent.

[A1]

The main hypothesis: for every real $ε > 0$ there is continuous $g_{ε}$ with $∣ f (x) - g_{ε} (x) ∣ < ε$ for all $x \in X$ .

[L1]

$f$ is continuous at $x_{0}$ iff for every open $V \subseteq R$ with $f (x_{0}) \in V$ there is open $U \subseteq X$ with $x_{0} \in U$ and $f [U] \subseteq V$ (Continuity of a map of topological spaces at a point and globally).

[L2]

[L3]

The bounded open intervals $(a - r, a + r)$ , $r > 0$ , are a basis for the usual topology of $R$ , so for open $V ∋ y_{0}$ there is real $r > 0$ with $(y_{0} - r, y_{0} + r) \subseteq V$ (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, claim 2 and 3, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not, 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, Basis and subbasis for a topology, and the topology generated by a family of sets).

[L4]

Triangle inequality: $∣ u + v ∣ \leq ∣ u ∣ + ∣ v ∣$ , hence $∣ u - w ∣ \leq ∣ u - v ∣ + ∣ v - w ∣$ for reals $u, v, w$ (The triangle inequality).

[L5]

Absolute value: $∣ u ∣ < c$ iff $- c < u < c$ , for real $c > 0$ ; and $- c \leq u \leq c$ iff $∣ u ∣ \leq c$ , for real $c \geq 0$ (Basic properties of the absolute value).

[L6]

Finite triangle inequality along a finite index set, iterating [L4]: $∣ \sum_{k} u_{k} ∣ \leq \sum_{k} ∣ u_{k} ∣$ (Basic properties of the absolute value, Ordered field).

[L7]

Comparison and absolute convergence: if $0 \leq a_{k} \leq b_{k}$ eventually and $\sum b_{k}$ converges then $\sum a_{k}$ converges (If $0 \leq a_{k} \leq b_{k}$ eventually, convergence of $\sum b_{k}$ gives convergence of $\sum a_{k}$ , and divergence of $\sum a_{k}$ gives divergence of $\sum b_{k}$ ); if $\sum ∣ a_{k} ∣$ converges then $\sum a_{k}$ converges (If $\sum ∣ a_{k} ∣$ converges then $\sum a_{k}$ converges).

[L8]

For a series of nonnegative terms, the partial sums are nondecreasing, bounded above by the sum when the series converges, and converge to the sum (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum, Series, partial sums, convergence and the sum, divergence, and the tail series).

[L9]

Limits in $R$ preserve non-strict order: if $a_{k} \to a$ and $a_{k} \leq c$ for all $k$ beyond some index, then $a \leq c$ (Sequence basics in an arbitrary ordered field: limits are unique, limits preserve non-strict inequalities, convergent sequences are Cauchy, Cauchy sequences are bounded, and a Cauchy sequence with a convergent subsequence converges).

Proof

technique · constructive

1.1

Fix $x_{0} \in X$ and an open $V \subseteq R$ with $f (x_{0}) \in V$ ; by [L3] fix a real $r > 0$ with $(f (x_{0}) - r, f (x_{0}) + r) \subseteq V$ .

givenL3choose

1.2

Let $g, h : X \to R$ be continuous, let $x_{1} \in X$ and let real $η > 0$ ; arguing directly from continuity of $g$ and of $h$ at $x_{1}$ (via [L1] and [L2]) separately, fix open $U_{1}, U_{2} ∋ x_{1}$ with $∣ g (x) - g (x_{1}) ∣ < η / 2$ on $U_{1}$ and $∣ h (x) - h (x_{1}) ∣ < η / 2$ on $U_{2}$ .

givenL1L2choose

1.3

Fix $x \in X$ . The real sequence $(g_{n} (x))_{n \in N}$ satisfies $0 \leq ∣ g_{n} (x) ∣ \leq M_{n}$ for every $n$ , and $\sum M_{n}$ converges by hypothesis, so [L7] gives that $\sum ∣ g_{n} (x) ∣$ converges, and hence $\sum g_{n} (x)$ converges; define $F (x) : = \sum_{n = 0}^{\infty} g_{n} (x)$ and $s_{N} (x) : = \sum_{n < N} g_{n} (x)$ , so $s_{N} (x) \to F (x)$ as $N \to \infty$ .

givenL7construct

1.4

Write $σ_{N} : = \sum_{n < N} M_{n}$ and $S : = \sum_{n = 0}^{\infty} M_{n}$ ; since $M_{n} \geq 0$ for every $n$ , [L8] gives that $(σ_{N})$ is nondecreasing with $σ_{N} \leq S$ for every $N$ , and $σ_{N} \to S$ . So $S - σ_{N} \geq 0$ for every $N$ and $S - σ_{N} \to 0$ ; given a real $ε > 0$ , fix $N \in N$ with $S - σ_{N} < ε$ .

givenL8choose

2.1

By [A1] applied with $ε : = r / 3 > 0$ , fix a continuous $g : X \to R$ with $∣ f (x) - g (x) ∣ < r / 3$ for every $x \in X$ .

step 1.1A1choose

2.2

$U_{1} \cap U_{2}$ is open, contains $x_{1}$ , and for $x \in U_{1} \cap U_{2}$ : $∣ (g + h) (x) - (g + h) (x_{1}) ∣ \leq ∣ g (x) - g (x_{1}) ∣ + ∣ h (x) - h (x_{1}) ∣ < η$ by [L4].

step 1.2L4algebra

2.3

For every $x \in X$ and every $K > N$ : $∣ s_{K} (x) - s_{N} (x) ∣ = ∣ \sum_{N \leq n < K} g_{n} (x) ∣ \leq \sum_{N \leq n < K} ∣ g_{n} (x) ∣ \leq \sum_{N \leq n < K} M_{n} = σ_{K} - σ_{N} \leq S - σ_{N}$ , by [L6], the hypothesis $∣ g_{n} (x) ∣ \leq M_{n}$ , and $σ_{K} \leq S$ from step 1.4.

step 1.4step 1.3L6algebra

3.1

$U : = g^{- 1} [(g (x_{0}) - r / 3, g (x_{0}) + r / 3)]$ is open by [L2], since $g$ is continuous by step 2.1, and $x_{0} \in U$ , since $∣ g (x_{0}) - g (x_{0}) ∣ = 0 < r / 3$ .

step 2.1L2

3.2

Since $x_{1} \in X$ and real $η > 0$ were arbitrary, $g + h$ is continuous on $X$ ; iterating this over finitely many further sums, any finite sum $g_{0} + \dots + g_{N - 1}$ of continuous real-valued functions on $X$ is continuous, for every $N \geq 1$ , with the case $N = 0$ (the zero function) continuous as a constant.

step 2.2

3.3

By step 2.3, $∣ s_{K} (x) - s_{N} (x) ∣ \leq S - σ_{N}$ for every $K > N$ ; as $K \to \infty$ , $s_{K} (x) \to F (x)$ by step 1.3, so [L9] applied to the two non-strict bounds $- (S - σ_{N}) \leq s_{K} (x) - s_{N} (x) \leq S - σ_{N}$ (equivalent to step 2.3 by [L5]) gives $- (S - σ_{N}) \leq F (x) - s_{N} (x) \leq S - σ_{N}$ , that is $∣ F (x) - s_{N} (x) ∣ \leq S - σ_{N} < ε$ by [L5] and step 1.4, for every $x \in X$ , with $N$ independent of $x$ .

step 2.3step 1.4step 1.3L5L9

4.1

For $x \in U$ : $∣ f (x) - f (x_{0}) ∣ \leq ∣ f (x) - g (x) ∣ + ∣ g (x) - g (x_{0}) ∣ + ∣ g (x_{0}) - f (x_{0}) ∣ < r / 3 + r / 3 + r / 3 = r$ , by [L4] (twice), step 2.1 (the first and third terms) and the defining property of $U$ (step 3.1, the middle term).

step 2.1step 3.1L4algebra

4.2

For $N \in N$ , $s_{N} = g_{0} + \dots + g_{N - 1}$ is a finite sum of continuous functions, hence continuous on $X$ , by step 3.2.

step 3.2

5.1

By step 4.1, $f (x) \in (f (x_{0}) - r, f (x_{0}) + r) \subseteq V$ for every $x \in U$ (step 1.1), so $f [U] \subseteq V$ ; with $U$ open and $x_{0} \in U$ (step 3.1), and $V$ an arbitrary open set containing $f (x_{0})$ (step 1.1), $f$ is continuous at $x_{0}$ by [L1].

step 4.1step 3.1step 1.1L1

6.1

Since $x_{0} \in X$ was arbitrary, $f$ is continuous on $X$ ; this proves the main clause.

step 5.1

7.1

Since $s_{N}$ is continuous by step 4.2 and real $ε > 0$ was arbitrary, the hypothesis of the main clause (steps 1.1–6.1) is met by $F$ , taking $g_{ε} : = s_{N}$ ; hence $F$ is continuous on $X$ . This, with step 1.3, proves the second clause.

step 3.3step 4.2step 6.1discharge-construct∎

Remarks

The $ε / 3$ split is the whole mechanism, and it is exactly the triangle inequality read three ways: once to compare $f$ with an approximant, once to use continuity of that approximant, and once to compare back. Nothing about $X$ is used beyond the definition of continuity; the hypothesis never mentions a metric on $X$ , only on the common target $R$ .
The second clause is the Weierstrass $M$ -test, stated only as far as this page needs it. It is not stated for a general metric or normed target, and it produces no rate of convergence beyond what step 1.4 already gives: a single $N$ , working uniformly in $x$ , for every tolerance $ε$ .
No choice principle beyond what a single real number requires is used anywhere above. Steps 1.1, 2.1 and 1.4 each fix one witness from a nonempty set of reals or a single continuous function, and no step selects simultaneously from an infinite family.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

Under dependent choice a space is perfectly normal if and only if it is normal and every closed set is a zero set

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). Let $(X, T)$ be a topological space. Then $X$ is perfectly normal (Completely normal ( $T_{5}$ ) and perfectly normal ( $T_{6}$ ) spaces) if and only if $X$ is normal (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly) and every closed subset of $X$ is a zero set (Zero sets and cozero sets of continuous real-valued functions).

Only the forward direction spends a choice principle beyond the dependent choice already inside Urysohn's lemma. Producing a Urysohn function for every level of a countable presentation $C = ⋂_{n} U_{n}$ , all at once, is in form an application of the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )); the argument below performs it as a direct instance of dependent choice itself, using a relation that does not depend on the previous term, so no hypothesis beyond DC is added and none is hidden. The converse direction uses no choice principle at all.

Facts & Assumptions

Given: A topological space $(X, T)$ and dependent choice; for the forward direction, $X$ perfectly normal; for the converse, $X$ normal with every closed subset a zero set.

[A1]

$D C$ : for every nonempty set $P$ , every relation $R \subseteq P \times P$ entire on $P$ , and every $a \in P$ , there is a sequence $(p_{k})_{k \in N}$ with $p_{0} = a$ and $p_{k} R p_{k + 1}$ for every $k$ (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[A2]

$X$ is perfectly normal exactly when $X$ is normal and every closed subset of $X$ is a $G_{δ}$ (Completely normal ( $T_{5}$ ) and perfectly normal ( $T_{6}$ ) spaces).

[L1]

$A \subseteq X$ is a $G_{δ}$ set when $A = ⋂_{n \in N} V_{n}$ for some open sets $V_{n}$ ( $G_{δ}$ and $F_{σ}$ subsets of a topological space, agreeing with the real-line notion).

[L2]

[L3]

For continuous $k : X \to R$ , $Z (k) : = k^{- 1} ({0})$ ; every zero set is closed and a $G_{δ}$ (Zero sets and cozero sets of continuous real-valued functions).

[L4]

The geometric series: $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ for real $∣ r ∣ < 1$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges); in particular $\sum_{k = 0}^{\infty} 2^{- (k + 1)} = \frac{1}{2} \sum_{k = 0}^{\infty} 2^{- k} = \frac{1}{2} \cdot \frac{1}{1 - \frac{1}{2}} = 1$ , a convergent series of positive reals (Series, partial sums, convergence and the sum, divergence, and the tail series).

[L5]

The $M$ -test: if $(g_{n})$ are continuous real-valued functions on $X$ , $(M_{n})$ nonnegative reals with $∣ g_{n} (x) ∣ \leq M_{n}$ for every $x$ and $n$ , and $\sum M_{n}$ converges, then $\sum g_{n} (x)$ converges for every $x \in X$ and $F : = \sum_{n} g_{n}$ is continuous on $X$ (If for every $ε > 0$ some continuous $g : X \to R$ satisfies $∣ f (x) - g (x) ∣ < ε$ for all $x$ , then $f$ is continuous; in particular a uniformly convergent series of continuous real functions has a continuous sum, second clause).

[L6]

Scalar multiple of a continuous map is continuous: for continuous $h : X \to R$ and real $c > 0$ , $x \mapsto c h (x)$ is continuous — given $x_{0} \in X$ and real $ε > 0$ , continuity of $h$ at $x_{0}$ with tolerance $ε / c$ gives open $U ∋ x_{0}$ with $∣ h (x) - h (x_{0}) ∣ < ε / c$ on $U$ , whence $∣ c h (x) - c h (x_{0}) ∣ = c ∣ h (x) - h (x_{0}) ∣ < ε$ on $U$ (Continuity of a map of topological spaces at a point and globally, For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ , Basic properties of the absolute value).

[L7]

Limits in $R$ preserve non-strict order: if $a_{k} \to a$ and $a_{k} \geq c$ for all $k$ beyond some index, then $a \geq c$ (Sequence basics in an arbitrary ordered field: limits are unique, limits preserve non-strict inequalities, convergent sequences are Cauchy, Cauchy sequences are bounded, and a Cauchy sequence with a convergent subsequence converges).

[L8]

For a series of nonnegative terms, the partial sums are nondecreasing (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum).

Proof

technique · constructive

1.1

Assume $X$ is perfectly normal.

assume-hyp

1.2

Assume instead that $X$ is normal and every closed subset of $X$ is a zero set.

assume-hyp

2.1

Under step 1.1: by [A2], $X$ is normal and every closed subset of $X$ is a $G_{δ}$ ; in particular $X$ is normal.

step 1.1A2

2.2

Under step 1.2: let $C \subseteq X$ be closed; by hypothesis $C$ is a zero set, hence $G_{δ}$ by [L3]. Since $C$ was arbitrary, every closed subset of $X$ is $G_{δ}$ ; with $X$ normal by hypothesis, $X$ is perfectly normal by [A2].

step 1.2L3A2

3.1

Under step 1.1: let $C \subseteq X$ be closed; by step 2.1, $C$ is $G_{δ}$ , so by [L1] fix open sets $(U_{n})_{n \in N}$ with $C = ⋂_{n} U_{n}$ .

step 2.1L1choose

4.1

Under step 1.1: put $P : = {(n, h) : n \in N, h : X \to [0, 1] continuous, C \subseteq h^{- 1} ({0}), X ∖ U_{n} \subseteq h^{- 1} ({1})}$ , and for $(n, h), (n^{'}, h^{'}) \in P$ say $(n, h) R (n^{'}, h^{'})$ when $n^{'} = n + 1$ . Since $C \subseteq U_{0}$ (step 3.1), $C$ and $X ∖ U_{0}$ are disjoint closed sets ( $X ∖ U_{0}$ closed, $U_{0}$ being open); by [L2] and step 2.1, fix $h_{0}$ with $(0, h_{0}) \in P$ .

step 2.1step 3.1L2chooseconstruct

4.2

Under step 1.1: for every $(n, h) \in P$ : $C \subseteq U_{n + 1}$ (step 3.1), so $C$ and $X ∖ U_{n + 1}$ are disjoint closed sets; by [L2] and step 2.1 there is $h^{'}$ with $(n + 1, h^{'}) \in P$ , so $(n, h) R (n + 1, h^{'})$ . Hence $R$ is entire on $P$ .

step 2.1step 3.1L2choose

5.1

Under step 1.1: $P$ is nonempty by step 4.1 and $R$ is entire on $P$ by step 4.2; by [A1] applied with $a : = (0, h_{0})$ , there is a sequence $((m_{k}, H_{k}))_{k \in N}$ with $(m_{0}, H_{0}) = (0, h_{0})$ and $(m_{k}, H_{k}) R (m_{k + 1}, H_{k + 1})$ for every $k$ . As $(n, h) R (n^{'}, h^{'})$ forces $n^{'} = n + 1$ , induction gives $m_{k} = k$ for every $k$ ; so $H_{k} : X \to [0, 1]$ is continuous with $C \subseteq H_{k}^{- 1} ({0})$ and $X ∖ U_{k} \subseteq H_{k}^{- 1} ({1})$ , for every $k \in N$ .

step 4.1step 4.2A1construct

6.1

Under step 1.1: for $k \in N$ put $g_{k} : = 2^{- (k + 1)} H_{k}$ ; by [L6] each $g_{k}$ is continuous, and $∣ g_{k} (x) ∣ = 2^{- (k + 1)} H_{k} (x) \leq 2^{- (k + 1)} = : M_{k}$ for every $x \in X$ , since $H_{k} (x) \in [0, 1]$ ; and $\sum M_{k}$ converges by [L4].

step 5.1L4L6construct

7.1

Under step 1.1: by [L5] applied to $(g_{k})$ and $(M_{k})$ of step 6.1: for every $x \in X$ the series $\sum g_{k} (x)$ converges, and $f : = \sum_{k = 0}^{\infty} g_{k}$ is a continuous map $X \to R$ .

step 6.1L5construct

7.2

Under step 1.1: for $x \notin C$ : since $C = ⋂_{n} U_{n}$ (step 3.1), there is a natural $m$ with $x \notin U_{m}$ , so $x \in X ∖ U_{m} \subseteq H_{m}^{- 1} ({1})$ (step 5.1), giving $H_{m} (x) = 1$ and $g_{m} (x) = 2^{- (m + 1)}$ .

step 3.1step 5.1step 6.1choose

8.1

Under step 1.1: for $x \in C$ : $H_{k} (x) = 0$ for every $k$ (step 5.1), so $g_{k} (x) = 0$ for every $k$ (step 6.1), and $f (x) = \sum_{k} 0 = 0$ .

step 5.1step 6.1step 7.1

8.2

Under step 1.1, continuing from step 7.2: every term $g_{k} (x) \geq 0$ , since $H_{k} (x) \in [0, 1]$ ; so by [L8] the partial sums $s_{N} (x) : = \sum_{k < N} g_{k} (x)$ satisfy $s_{N} (x) \geq g_{m} (x) = 2^{- (m + 1)}$ for every $N > m$ , and $s_{N} (x) \to f (x)$ by step 7.1; so [L7] gives $f (x) \geq 2^{- (m + 1)} > 0$ .

step 7.2step 7.1L7L8

9.1

Under step 1.1: steps 8.1 and 8.2 give $f (x) = 0$ for $x \in C$ and $f (x) \neq 0$ for $x \notin C$ , so $C = f^{- 1} ({0}) = Z (f)$ , a zero set by [L3]. Since $C$ was an arbitrary closed subset of $X$ , every closed subset of $X$ is a zero set.

step 8.1step 8.2L3

10.1

Steps 2.1 and 9.1 show that, under the hypothesis of step 1.1, $X$ is normal and every closed subset of $X$ is a zero set.

step 2.1step 9.1

11.1

Steps 10.1 and 2.2 establish the two directions of the stated equivalence.

step 10.1step 2.2discharge-construct∎

Remarks

The construction of step 4.1–5.1 is exactly the standard proof that dependent choice implies countable choice, specialised to the family of admissible Urysohn functions at each level: the relation $R$ never looks at the first coordinate's function, only at its index, so any admissible successor is accepted. This is why the theorem needs no hypothesis beyond DC, even though the step it performs — choosing one function per natural number, all at once — is the shape of ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).
The series $\sum 2^{- (k + 1)} H_{k}$ , not $\sum 2^{- k} H_{k}$ , is what starts at value $1$ . Indexing from $k = 0$ with weight $2^{- (k + 1)}$ makes the total weight exactly $1$ and keeps every weight strictly positive, which is what step 8.2 needs to conclude $f (x) > 0$ off $C$ from a single nonzero term.
The converse costs nothing beyond what is already on the separation-axioms page. "Every zero set is a $G_{δ}$ " is proved as part of Zero sets and cozero sets of continuous real-valued functions; step 2.2 only specialises it to the closed sets that the hypothesis already promises are zero sets.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)Open item page →

Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a, b]$ extends continuously to the whole space, and this property characterises normality

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). Let $(X, T)$ be a topological space.

If $X$ is normal (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly), $A \subseteq X$ is closed (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) and $a \leq b$ are reals, then every continuous $f : A \to [a, b]$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) extends to a continuous $F : X \to [a, b]$ with $F ∣_{A} = f$ .
Conversely, if for every closed $A \subseteq X$ and every reals $a \leq b$ every continuous $f : A \to [a, b]$ extends to a continuous $F : X \to [a, b]$ with $F ∣_{A} = f$ , then $X$ is normal. This direction uses no choice principle.

Facts & Assumptions

Given: A topological space $(X, T)$ and dependent choice; for clause 1, $X$ normal, $A \subseteq X$ closed, reals $a \leq b$ , and continuous $f : A \to [a, b]$ ; for clause 2, $X$ such that the extension property of clause 1 holds for every closed subspace and every $a \leq b$ .

[A1]

$D C$ : for every nonempty set $P$ , every relation $R$ entire on $P$ , and every $a \in P$ , there is a sequence $(p_{k})_{k \in N}$ with $p_{0} = a$ and $p_{k} R p_{k + 1}$ for every $k$ (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[A2]

Normal: 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).

[L1]

Urysohn's lemma, clause 1: assuming DC, if $X$ is normal and $P, Q \subseteq X$ are disjoint closed sets, there is a continuous $h : X \to [0, 1]$ with $P \subseteq h^{- 1} ({0})$ , $Q \subseteq h^{- 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).

[L2]

If $A$ is closed in $X$ and $C \subseteq A$ is closed in the subspace $A$ , then $C$ is closed in $X$ : by 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 $C = F \cap A$ for some closed $F \subseteq X$ , and an intersection of two closed sets of $X$ is closed (Interior, closure, boundary, exterior, derived set and isolated point in a topological space, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L3]

Preimages of closed sets under a continuous map are closed (For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ , clause (c)); preimages of open sets are open (clause (b)).

[L4]

The geometric series: $\sum_{n \geq 0} (2 / 3)^{n} = 1 / (1 - 2 / 3) = 3$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges), so $\sum_{n \geq 0} M_{n} / 3 = r$ for $M_{n} : = r (2 / 3)^{n}$ and any real $r$ ; and $(2 / 3)^{n} \to 0$ as $n \to \infty$ (the same theorem's proof, For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

[L5]

The $M$ -test: continuous $(g_{n})$ on $X$ , nonnegative reals $(N_{n})$ with $∣ g_{n} (x) ∣ \leq N_{n}$ for all $x, n$ and $\sum N_{n}$ convergent, give $\sum g_{n} (x)$ convergent for every $x$ and $\sum_{n} g_{n}$ continuous on $X$ (If for every $ε > 0$ some continuous $g : X \to R$ satisfies $∣ f (x) - g (x) ∣ < ε$ for all $x$ , then $f$ is continuous; in particular a uniformly convergent series of continuous real functions has a continuous sum, second clause).

[L6]

Finite triangle inequality $∣ \sum_{k} u_{k} ∣ \leq \sum_{k} ∣ u_{k} ∣$ (Basic properties of the absolute value); a real sequence has at most one limit, and limits preserve non-strict order (Sequence basics in an arbitrary ordered field: limits are unique, limits preserve non-strict inequalities, convergent sequences are Cauchy, Cauchy sequences are bounded, and a Cauchy sequence with a convergent subsequence converges).

[L7]

[L8]

$A$ and $B$ open in a subspace $S$ , with $A \cup B = S$ and $A \cap B = \emptyset$ : a function on $S$ constant on $A$ and constant on $B$ is continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, clause 2).

Proof

technique · constructive

1.1

Assume $X$ is normal, $A \subseteq X$ is closed, $a \leq b$ are reals, and $f : A \to [a, b]$ is continuous.

assume-hyp

1.2

Assume instead that $X$ is such that every continuous $g : C \to [p, q]$ on a closed $C \subseteq X$ , $p \leq q$ reals, extends continuously to $X \to [p, q]$ .

assume-hyp

2.1

Under step 1.1: if $a = b$ the constant map $F : X \to {a} \subseteq [a, b]$ , $F \equiv a$ , is continuous and $F ∣_{A} = f$ , since $f : A \to {a}$ forces $f \equiv a$ . Assume from here that $a < b$ .

step 1.1assume-hypconstruct

2.2

Under step 1.2: let $C, E \subseteq X$ be disjoint closed sets; $C \cup E$ is closed, and $C, E$ are each open in the subspace $C \cup E$ , being the complement there of the other, which is closed. Define $k : C \cup E \to {0, 1} \subseteq [0, 1]$ by $k \equiv 0$ on $C$ and $k \equiv 1$ on $E$ ; $k$ is constant, hence continuous, on each of $C$ and $E$ , so $k$ is continuous on $C \cup E$ by [L8].

step 1.2L8chooseconstruct

3.1

Under steps 1.1 and 2.1: put $c : = (a + b) / 2$ and $r : = (b - a) / 2 > 0$ , and define $f_{0} : A \to R$ by $f_{0} (x) : = f (x) - c$ ; $f_{0}$ is continuous, being $f$ minus a constant, and $f_{0} [A] \subseteq [- r, r]$ , since $f [A] \subseteq [a, b] = [c - r, c + r]$ .

step 1.1step 2.1algebraconstruct

3.2

Under step 1.2: by hypothesis applied to the closed set $C \cup E$ and $p : = 0, q : = 1$ , fix a continuous $K : X \to [0, 1]$ with $K ∣_{C \cup E} = k$ .

step 1.2step 2.2choose

4.1

Under step 1.1: for $n \in N$ put $M_{n} : = r (2 / 3)^{n}$ . Call a pair $(f_{n}, g_{n})$ , with $f_{n} : A \to R$ and $g_{n} : X \to R$ continuous, admissible at level $n$ when $∣ f_{n} (x) ∣ \leq M_{n}$ for $x \in A$ ; $∣ g_{n} (x) ∣ \leq M_{n} / 3$ for $x \in X$ ; $g_{n} (x) = - M_{n} / 3$ for $x \in A$ with $f_{n} (x) \leq - M_{n} / 3$ ; and $g_{n} (x) = M_{n} / 3$ for $x \in A$ with $f_{n} (x) \geq M_{n} / 3$ .

step 3.1construct

4.2

Under step 1.2: by [L7], put $O_{1} : = K^{- 1} ([0, \frac{1}{2}))$ , $O_{2} : = K^{- 1} ((\frac{1}{2}, 1])$ , open by [L3]. $C \subseteq O_{1}$ , since $K \equiv 0 \in [0, \frac{1}{2})$ on $C$ ; $E \subseteq O_{2}$ , since $K \equiv 1 \in (\frac{1}{2}, 1]$ on $E$ ; and $O_{1} \cap O_{2} = \emptyset$ , the two target sets being disjoint.

step 3.2L7L3

5.1

Under step 1.1: put $A_{0}^{-} : = {x \in A : f_{0} (x) \leq - M_{0} / 3}$ , $A_{0}^{+} : = {x \in A : f_{0} (x) \geq M_{0} / 3}$ ; both closed in $A$ by [L3] and hence in $X$ by [L2], and disjoint since $- M_{0} / 3 < M_{0} / 3$ . By [L1] fix continuous $h_{0} : X \to [0, 1]$ with $A_{0}^{-} \subseteq h_{0}^{- 1} ({0})$ and $A_{0}^{+} \subseteq h_{0}^{- 1} ({1})$ , and put $g_{0} : = (M_{0} / 3) (2 h_{0} - 1)$ , continuous.

step 3.1step 4.1L1L2L3chooseconstruct

5.2

Under step 1.1: let $n \in N$ and let $(f_{n}, g_{n})$ be admissible at level $n$ ; define $f_{n + 1} : A \to R$ by $f_{n + 1} (x) : = f_{n} (x) - g_{n} (x)$ , continuous.

step 4.1construct

5.3

Under step 1.2: since $C, E$ were an arbitrary disjoint closed pair, step 4.2 exhibits disjoint open supersets for every such pair, so $X$ is normal by [A2]; this is clause 2, and it uses [A1] nowhere.

step 4.2A2

6.1

Under step 1.1: $(f_{0}, g_{0})$ is admissible at level $0$ : $∣ f_{0} ∣ \leq M_{0}$ on $A$ by step 3.1; $∣ g_{0} (x) ∣ = (M_{0} / 3) ∣ 2 h_{0} (x) - 1 ∣ \leq M_{0} / 3$ for every $x$ , since $h_{0} (x) \in [0, 1]$ ; $g_{0} (x) = - M_{0} / 3$ for $x \in A_{0}^{-}$ , where $h_{0} (x) = 0$ ; and $g_{0} (x) = M_{0} / 3$ for $x \in A_{0}^{+}$ , where $h_{0} (x) = 1$ .

step 5.1algebra

6.2

Under step 1.1, continuing under step 5.2: for $x \in A$ with $f_{n} (x) \leq - M_{n} / 3$ : $g_{n} (x) = - M_{n} / 3$ (admissibility), so $f_{n + 1} (x) = f_{n} (x) + M_{n} / 3 \in [- 2 M_{n} / 3, 0]$ , using $- M_{n} \leq f_{n} (x) \leq - M_{n} / 3$ ; for $x \in A$ with $f_{n} (x) \geq M_{n} / 3$ : $f_{n + 1} (x) = f_{n} (x) - M_{n} / 3 \in [0, 2 M_{n} / 3]$ ; for $x \in A$ with $- M_{n} / 3 < f_{n} (x) < M_{n} / 3$ : $∣ g_{n} (x) ∣ \leq M_{n} / 3$ gives $f_{n + 1} (x) \in (- 2 M_{n} / 3, 2 M_{n} / 3)$ . In every case $∣ f_{n + 1} (x) ∣ \leq 2 M_{n} / 3 = M_{n + 1}$ .

step 5.2step 4.1algebra

6.3

Under step 1.1: put $A_{n + 1}^{-} : = {x \in A : f_{n + 1} (x) \leq - M_{n + 1} / 3}$ , $A_{n + 1}^{+} : = {x \in A : f_{n + 1} (x) \geq M_{n + 1} / 3}$ ; closed in $X$ by [L2], [L3], and disjoint. By [L1] fix continuous $h_{n + 1} : X \to [0, 1]$ with $A_{n + 1}^{-} \subseteq h_{n + 1}^{- 1} ({0})$ , $A_{n + 1}^{+} \subseteq h_{n + 1}^{- 1} ({1})$ , and put $g_{n + 1} : = (M_{n + 1} / 3) (2 h_{n + 1} - 1)$ .

step 5.2step 4.1L1L2L3chooseconstruct

7.1

Under step 1.1: $(f_{n + 1}, g_{n + 1})$ is admissible at level $n + 1$ , by step 6.2 and the same computation as step 6.1 with $h_{n + 1}, g_{n + 1}, M_{n + 1}$ in place of $h_{0}, g_{0}, M_{0}$ . So every admissible pair at level $n$ has an admissible successor at level $n + 1$ .

step 6.2step 6.3

8.1

Under step 1.1: put $P : = {(n, f_{n}, g_{n}) : n \in N, (f_{n}, g_{n}) admissible at level n}$ , and for $(n, f, g), (n^{'}, f^{'}, g^{'}) \in P$ say $(n, f, g) R (n^{'}, f^{'}, g^{'})$ when $n^{'} = n + 1$ and $f^{'} = (f - g) ∣_{A}$ pointwise. $P$ is nonempty by step 6.1, and $R$ is entire on $P$ by steps 5.2, 6.2, 6.3 and 7.1 (the pair produced there has $f_{n + 1} = (f_{n} - g_{n}) ∣_{A}$ exactly as step 5.2 defines it). By [A1] with $a : = (0, f_{0}, g_{0})$ , fix a sequence $((n_{k}, F_{k}, G_{k}))_{k \in N}$ with $(n_{0}, F_{0}, G_{0}) = (0, f_{0}, g_{0})$ and $(n_{k}, F_{k}, G_{k}) R (n_{k + 1}, F_{k + 1}, G_{k + 1})$ for every $k$ ; as $R$ forces $n^{'} = n + 1$ , induction gives $n_{k} = k$ , so $(F_{k}, G_{k})$ is admissible at level $k$ for every $k$ , with $F_{k + 1} = (F_{k} - G_{k}) ∣_{A}$ .

step 6.1step 7.1step 5.2A1construct

9.1

Under step 1.1: by [L4], $\sum_{n} M_{n} / 3 = r$ , convergent; by [L5] applied to $(G_{n})$ and $(M_{n} / 3)$ (each $∣ G_{n} (x) ∣ \leq M_{n} / 3$ for all $x$ , by admissibility), for every $x \in X$ the series $\sum_{n} G_{n} (x)$ converges, and $F : = \sum_{n = 0}^{\infty} G_{n}$ is a continuous map $X \to R$ .

step 8.1L4L5construct

9.2

Under step 1.1: for $x \in A$ and $N \in N$ : by the telescoping of step 8.1, $\sum_{n < N} G_{n} (x) = F_{0} (x) - F_{N} (x) = f_{0} (x) - F_{N} (x)$ , since $F_{0} = f_{0}$ .

step 8.1algebra

10.1

Under step 1.1: for every $x \in X$ and $N \in N$ , $∣ \sum_{n < N} G_{n} (x) ∣ \leq \sum_{n < N} ∣ G_{n} (x) ∣ \leq \sum_{n < N} M_{n} / 3 \leq r$ , by [L6] and admissibility; letting $N \to \infty$ , since $\sum_{n < N} G_{n} (x) \to F (x)$ (step 9.1) and order is preserved in the limit ([L6]), $∣ F (x) ∣ \leq r$ .

step 9.1L4L6algebra

10.2

Under step 1.1: for $x \in A$ : $∣ F_{N} (x) ∣ \leq M_{N} = r (2 / 3)^{N} \to 0$ as $N \to \infty$ , by admissibility of $F_{N}$ (step 8.1) and [L4]; so by step 9.2, $\sum_{n < N} G_{n} (x) = f_{0} (x) - F_{N} (x) \to f_{0} (x) - 0 = f_{0} (x)$ .

step 9.2step 8.1L4

11.1

Under step 1.1: for $x \in A$ : $\sum_{n < N} G_{n} (x) \to F (x)$ by step 9.1 and $\to f_{0} (x)$ by step 10.2; since a real sequence has at most one limit ([L6]), $F (x) = f_{0} (x)$ .

step 9.1step 10.2L6

12.1

Under step 1.1: define $\hat{F} : X \to R$ by $\hat{F} (x) : = F (x) + c$ , continuous; for $x \in X$ , $\hat{F} (x) \in [c - r, c + r] = [a, b]$ by step 10.1; for $x \in A$ , $\hat{F} (x) = F (x) + c = f_{0} (x) + c = f (x)$ by step 11.1 and the definition of $f_{0}$ in step 3.1.

step 10.1step 11.1step 3.1algebraconstruct

13.1

Steps 2.1 and 12.1 show that, under the hypothesis of step 1.1, a continuous $F : X \to [a, b]$ with $F ∣_{A} = f$ exists — either the constant map of step 2.1 when $a = b$ , or $\hat{F}$ of step 12.1 when $a < b$ — which is clause 1.

step 2.1step 12.1

14.1

Steps 13.1 and 5.3 establish clauses 1 and 2 respectively.

step 13.1step 5.3discharge-construct∎

Remarks

The bound after $n$ stages is $M_{n} = r (2 / 3)^{n}$ , with $M_{0} = r$ , not $r (2 / 3)^{n - 1}$ . Indexing from $n = 0$ is what makes step 6.1 the base case rather than a special first step, and it is why the geometric series of [L4] is summed from $n = 0$ .
Choice is spent once more here, genuinely as dependent choice and not in disguise. Unlike the countable-choice step inside the previous item, the function $g_{n + 1}$ chosen in step 6.3 depends on $f_{n + 1}$ , which is computed from $f_{n}$ and the particular $g_{n}$ retained in the state $(n, f_{n}, g_{n}) \in P$ of step 8.1 — not merely on the index $n$ . So the relation $R$ genuinely cannot be replaced by one that ignores its first argument, and this is exactly the situation dependent choice, rather than countable choice alone, is for.
The target $[a, b]$ is handled by a shift, not a rescaling. Working with $f_{0} = f - c$ keeps every bound in the construction a plain multiple of $r$ , and the final translation $\hat{F} = F + c$ is the only place $c$ reappears; no affine change of variable on $X$ or on $g_{n}$ is needed elsewhere.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

Under dependent choice, a continuous real-valued map on a closed subspace of a normal space extends to the whole space, and a map into an open interval extends into that same open interval

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). Let $(X, T)$ be normal (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly) and let $A \subseteq X$ be closed (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).

Every continuous $f : A \to R$ extends to a continuous $F : X \to R$ with $F ∣_{A} = f$ .
For reals $a < b$ , every continuous $f : A \to (a, b)$ extends to a continuous $F : X \to (a, b)$ with $F ∣_{A} = f$ .

Scope. The two one-sided open interval forms of Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, $(a, \infty)$ and $(- \infty, b)$ , are not treated by clause 2 above; extending it to them would need an explicit order-homeomorphism between a ray and $R$ , which is not built here.

Facts & Assumptions

Given: Dependent choice, a normal $(X, T)$ , a closed $A \subseteq X$ ; for clause 1, continuous $f : A \to R$ ; for clause 2, reals $a < b$ and continuous $f : A \to (a, b)$ .

[L1]

Tietze's extension theorem, clause 1: assuming DC, if $X$ is normal, $A$ closed and $p \leq q$ reals, every continuous $h : A \to [p, q]$ extends to continuous $H : X \to [p, q]$ with $H ∣_{A} = h$ (Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a, b]$ extends continuously to the whole space, and this property characterises normality).

[L2]

Urysohn's lemma, clause 1: assuming DC, disjoint closed $P, Q \subseteq X$ admit continuous $φ : X \to [0, 1]$ with $P \subseteq φ^{- 1} ({0})$ , $Q \subseteq φ^{- 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).

[L3]

Product of two continuous real-valued maps on $X$ is continuous: for continuous $g, h : X \to R$ and $x_{0} \in X$ , fix (continuity of $g$ ) open $U_{0} ∋ x_{0}$ with $∣ g (x) - g (x_{0}) ∣ < 1$ on $U_{0}$ , so $∣ g (x) ∣ < ∣ g (x_{0}) ∣ + 1 = : B$ there; for real $ε > 0$ fix open $U_{1} ∋ x_{0}$ with $∣ g (x) - g (x_{0}) ∣ < ε / (2 (∣ h (x_{0}) ∣ + 1))$ and open $U_{2} ∋ x_{0}$ with $∣ h (x) - h (x_{0}) ∣ < ε / (2 B)$ ; on $U_{0} \cap U_{1} \cap U_{2}$ , $∣ g (x) h (x) - g (x_{0}) h (x_{0}) ∣ \leq ∣ g (x) ∣ ∣ h (x) - h (x_{0}) ∣ + ∣ h (x_{0}) ∣ ∣ g (x) - g (x_{0}) ∣ < B \cdot ε / (2 B) + ∣ h (x_{0}) ∣ \cdot ε / (2 (∣ h (x_{0}) ∣ + 1)) < ε$ , so $g h$ is continuous at $x_{0}$ (Continuity of a map of topological spaces at a point and globally, Basic properties of the absolute value).

[L4]

Algebra of continuous real functions on $A \subseteq R$ : sums, scalar multiples, products, absolute values and quotients with nonvanishing denominator of continuous functions are continuous, as are constants and the identity (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

[L5]

For $S, T \subseteq R$ , a map $h : S \to T$ is continuous in the sense of Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point if and only if it is continuous as a map of topological spaces (subspace topologies of $R$ ), by Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace clause 1 (real $\Leftrightarrow$ metric continuity) together with Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not (metric $\Leftrightarrow$ topological continuity for a metrizable space).

[L6]

Preimages of closed (open) sets under a continuous map are closed (open) (For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ ).

[L7]

Composites of continuous maps are continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, clause 1).

Proof

technique · constructive

1.1

Fix reals $a < b$ . Define $α : (a, b) \to (- 1, 1)$ by $α (t) : = (2 t - a - b) / (b - a)$ and $β : (- 1, 1) \to (a, b)$ by $β (s) : = ((b - a) s + a + b) / 2$ ; both are continuous real functions by [L4], the denominators $b - a$ and $2$ being nonzero. Direct substitution gives $β (α (t)) = t$ for $t \in (a, b)$ and $α (β (s)) = s$ for $s \in (- 1, 1)$ .

givenL4algebraconstruct

1.2

Let $g : A \to (- 1, 1)$ be continuous, regarded as a map $A \to [- 1, 1]$ ; by [L1] with $p = - 1, q = 1$ fix continuous $G : X \to [- 1, 1]$ with $G ∣_{A} = g$ .

givenL1chooseconstruct

1.3

Define $ψ : (- 1, 1) \to R$ by $ψ (t) : = t / (1 - ∣ t ∣)$ and $χ : R \to (- 1, 1)$ by $χ (s) : = s / (1 + ∣ s ∣)$ ; both are continuous real functions by [L4], the denominators $1 - ∣ t ∣$ (on $(- 1, 1)$ ) and $1 + ∣ s ∣$ (everywhere) being positive. For $t \geq 0$ in $(- 1, 1)$ : $ψ (t) = t / (1 - t) \geq 0$ and $χ (ψ (t)) = \frac{t / (1 - t)}{1 + t / (1 - t)} = \frac{t / (1 - t)}{1 / (1 - t)} = t$ ; for $t < 0$ the same computation with $∣ t ∣ = - t$ gives $χ (ψ (t)) = t$ . Likewise $ψ (χ (s)) = s$ for every real $s$ , splitting on the sign of $s$ .

givenL4algebraconstruct

2.1

By [L5], $α$ and $β$ of step 1.1 are continuous as maps of topological spaces $(a, b) \to (- 1, 1)$ and $(- 1, 1) \to (a, b)$ .

step 1.1L5

2.2

Put $D : = G^{- 1} ({- 1, 1})$ , closed by [L6]; $D \cap A = \emptyset$ , since $G ∣_{A} = g$ takes values in $(- 1, 1)$ . By [L2], fix continuous $φ : X \to [0, 1]$ with $D \subseteq φ^{- 1} ({0})$ and $A \subseteq φ^{- 1} ({1})$ .

step 1.2L2L6choose

2.3

By [L5], $ψ$ and $χ$ of step 1.3 are continuous as maps of topological spaces $(- 1, 1) \to R$ and $R \to (- 1, 1)$ .

step 1.3L5

3.1

Define $\tilde{G} : X \to R$ by $\tilde{G} (x) : = φ (x) G (x)$ , continuous by [L3]. For $x \in A$ : $φ (x) = 1$ , so $\tilde{G} (x) = G (x) = g (x)$ . For $x \notin D$ : $∣ G (x) ∣ < 1$ and $φ (x) \in [0, 1]$ , so $∣ \tilde{G} (x) ∣ = φ (x) ∣ G (x) ∣ \leq ∣ G (x) ∣ < 1$ . For $x \in D$ : $φ (x) = 0$ , so $\tilde{G} (x) = 0$ . So $\tilde{G} : X \to (- 1, 1)$ and $\tilde{G} ∣_{A} = g$ .

step 2.2step 1.2L3construct

4.1

[Clause 2.] With $α, β$ as in steps 1.1–2.1: $g : = α \circ f : A \to (- 1, 1)$ is continuous by [L7]; by step 3.1 fix continuous $\tilde{G} : X \to (- 1, 1)$ with $\tilde{G} ∣_{A} = g$ ; define $F : = β \circ \tilde{G} : X \to (a, b)$ , continuous by [L7]. For $x \in A$ : $F (x) = β (\tilde{G} (x)) = β (g (x)) = β (α (f (x))) = f (x)$ by step 1.1. So $F$ extends $f$ into $(a, b)$ .

step 2.1step 3.1step 1.1L7algebraconstruct

4.2

[Clause 1.] Let $f : A \to R$ be continuous. With $ψ, χ$ as in steps 1.3 and 2.3: $g : = χ \circ f : A \to (- 1, 1)$ is continuous by [L7]; by step 3.1 fix continuous $\tilde{G} : X \to (- 1, 1)$ with $\tilde{G} ∣_{A} = g$ ; define $F : = ψ \circ \tilde{G} : X \to R$ , continuous by [L7]. For $x \in A$ : $F (x) = ψ (\tilde{G} (x)) = ψ (g (x)) = ψ (χ (f (x))) = f (x)$ by step 1.3. So $F$ extends $f$ into $R$ .

step 2.3step 3.1step 1.3L7algebraconstruct

5.1

Steps 4.1 and 4.2 establish clauses 2 and 1 respectively.

step 4.1step 4.2discharge-construct∎

Remarks

The affine maps of step 1.1 and the rational maps of step 1.3 play the same role: each turns a target interval into $(- 1, 1)$ or back, so that the single boundary-avoidance construction of steps 1.2, 2.2 and 3.1 need be proved once and reused for both clauses. Neither clause repeats that construction.
The product fact [L3] is the only piece of "algebra of continuous functions" this page needs for a map out of a general topological space; the sum and scalar-multiple facts used elsewhere on this page are proved where they are first needed, by the same style of argument.
Choice is spent only through [L1] and [L2], that is, only through the two cited results; nothing in steps 1.1–5.1 performs a further selection from an infinite family.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

Under dependent choice a locally compact Hausdorff space is completely regular, hence Tychonoff

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). If $(X, T)$ is locally compact (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space) 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 completely regular (Completely regular spaces and Tychonoff ( $T_{3 \frac{1}{2}}$ ) spaces), and hence, being Hausdorff, $X$ is Tychonoff.

The proof passes through the one-point compactification (The one-point (Alexandroff) compactification $X^{*} = X \cup {\infty}$ , whose open sets are the open sets of $X$ together with the complements in $X^{*}$ of the closed compact subsets of $X$ ) rather than through a hereditary property of regularity or complete regularity: none is used or needed.

Facts & Assumptions

Given: A locally compact Hausdorff space $(X, T)$ , a closed set $C \subseteq X$ , and a point $x_{0} \in X ∖ C$ .

[A1]

$X$ is locally compact (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space) and Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).

[L1]

The one-point compactification $X^{*} = X \cup {\infty}$ of a locally compact Hausdorff space $X$ : its open sets are the open sets of $X$ together with the sets $X^{*} ∖ K$ for $K$ a closed compact subset of $X$ (The one-point (Alexandroff) compactification $X^{*} = X \cup {\infty}$ , whose open sets are the open sets of $X$ together with the complements in $X^{*}$ of the closed compact subsets of $X$ ); consequently its closed sets are ${F \cup {\infty} : F closed in X}$ together with ${K : K closed compact in X}$ , the complements of the two families of open sets.

[L2]

$X^{*}$ is compact and contains $X$ as an open subspace (so the subspace topology $X$ inherits from $X^{*}$ is its own topology $T$ ); and $X^{*}$ is Hausdorff, since $X$ is locally compact and Hausdorff ( $X^{*}$ is compact and contains $X$ as an open subspace; $X$ is dense in $X^{*}$ exactly when $X$ is not compact; and $X^{*}$ is Hausdorff exactly when $X$ is locally compact and Hausdorff).

[L3]

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}$ ).

[L4]

[L5]

Urysohn's lemma, clause 1: assuming DC, a normal space's disjoint closed sets admit a continuous $[0, 1]$ -valued separating function (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).

[L6]

If $g : X^{*} \to Y$ is continuous and $X \subseteq X^{*}$ carries the subspace topology, then $g ∣_{X}$ is continuous (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).

[L7]

Completely regular: for closed $C$ and $x_{0} \notin C$ , a continuous $f : X \to [0, 1]$ with $f (x_{0}) = 1$ and $f \equiv 0$ on $C$ (Completely regular spaces and Tychonoff ( $T_{3 \frac{1}{2}}$ ) spaces).

Proof

technique · direct

1.1

By [L2], $X^{*}$ is compact and Hausdorff; by [L3], $X^{*}$ is regular and normal, hence $T_{3}$ and $T_{4}$ , that is normal and $T_{1}$ .

A1L2L3

1.2

$C \cup {\infty}$ is closed in $X^{*}$ : $C$ is closed in $X$ (given), so $C \cup {\infty}$ is one of the sets $F \cup {\infty}$ of [L1] with $F = C$ .

givenL1

1.3

${x_{0}}$ and $C \cup {\infty}$ are disjoint: $x_{0} \in X$ , so $x_{0} \neq \infty$ , and $x_{0} \notin C$ (given).

given

1.4

For $x \neq y$ in $X$ , Hausdorffness (given, [A1]) supplies disjoint open $U ∋ x$ , $V ∋ y$ ; then $y \notin U$ (else $y \in U \cap V = \emptyset$ ) and $x \notin V$ similarly, so $X$ is $T_{1}$ ( $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces).

2.1

By step 1.1 ( $T_{1}$ ) and [L4], ${x_{0}} \subseteq X \subseteq X^{*}$ is closed in $X^{*}$ .

step 1.1L4

3.1

By step 1.1 ( $X^{*}$ normal), steps 2.1, 1.2 and 1.3, and [L5], fix a continuous $g : X^{*} \to [0, 1]$ with $C \cup {\infty} \subseteq g^{- 1} ({0})$ and ${x_{0}} \subseteq g^{- 1} ({1})$ .

step 1.1step 2.1step 1.2step 1.3L5choose

4.1

By [L6] and [L2] ( $X$ a subspace of $X^{*}$ with its own topology), $f : = g ∣_{X} : X \to [0, 1]$ is continuous. For $x \in C$ : $x \in C \cup {\infty}$ , so $f (x) = g (x) = 0$ ; and $f (x_{0}) = g (x_{0}) = 1$ , since $x_{0} \in {x_{0}} \subseteq g^{- 1} ({1})$ .

step 3.1L2L6

5.1

Since $C$ and $x_{0} \notin C$ were arbitrary, step 4.1 exhibits, for every closed $C \subseteq X$ and $x_{0} \in X ∖ C$ , a continuous $f : X \to [0, 1]$ with $f (x_{0}) = 1$ , $f \equiv 0$ on $C$ ; by [L7], $X$ is completely regular.

step 4.1L7

6.1

By steps 5.1 and 1.4, $X$ is completely regular and $T_{1}$ , that is Tychonoff.

step 5.1step 1.4∎

Remarks

Only two facts about $X^{*}$ are used: that it is compact Hausdorff (so normal, via A compact Hausdorff space is regular and normal, hence $T_{3}$ and $T_{4}$ ), and that $X$ sits inside it as an open subspace with its own topology, so that a Urysohn function on $X^{*}$ restricts to one on $X$ with no further argument. No property of $X^{*}$ beyond these two, and no hereditary behaviour of regularity, complete regularity or normality, is used anywhere in the proof.
The choice principle is the one already inside Urysohn's lemma, applied once, inside the compact Hausdorff space $X^{*}$ ; nothing above performs a further selection.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

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 $N$ -indexed chain). Let $(X, 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, 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.

RemarkRemark: AI-generatedProof: Not applicableverified 2026-08-09 (gpt-5.6-terra-codex-subscription)‡ rests on unproved materialOpen item page →

Which results on this page spend dependent choice, which spend countable choice, and which are theorems of ZF

This remark extends the choice-strength bookkeeping of The proved choice ledger: hypotheses, equivalences, and upper bounds and of Conventions on this page, and the one implication of the classical chain that is not available at this point in the reading order §4 to the results proved on this page, naming exactly which theorem spends which principle and at which single step, in the spirit both of those items.

What is proved free of any choice principle

The dyadic rationals of $[0, 1]$ , their finite levels $D_{n}$ , and their density in $[0, 1]$ is choice free: its density argument fixes one natural number via The well-ordering principle, a theorem of ZF, and one dyadic rational via a single existential instantiation, never a simultaneous selection.

If $(U_{r})_{r \in D}$ are open with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ and $U_{1} = X$ , then $x \mapsto \inf {r \in D : x \in U_{r}}$ is a continuous map $X \to [0, 1]$ , and no choice principle is used is choice free by its own statement: given an already constructed family of open sets, producing the continuous function they define costs nothing. It is exactly because this step is free that the choice cost 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 can be isolated to the single step that builds the family in the first place.

The converse clauses — that a space whose disjoint closed sets are always separated by a continuous function is normal (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, clause 2), and that a space with the closed-subspace extension property is normal (Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a, b]$ extends continuously to the whole space, and this property characterises normality, clause 2) — use no choice principle: each cuts a given continuous function at the value $1 / 2$ and reads off two disjoint open sets.

If for every $ε > 0$ some continuous $g : X \to R$ satisfies $∣ f (x) - g (x) ∣ < ε$ for all $x$ , then $f$ is continuous; in particular a uniformly convergent series of continuous real functions has a continuous sum is choice free throughout, including its Weierstrass-type second clause: every existential step draws from a single nonempty set of reals or a single continuous function, never from an infinite family at once.

What spends dependent choice, and at which single step

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, clause 1, spends dependent choice exactly once: the application of The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain that strings together the countably many admissible finite-level open-set assignments built in that item's own proof, each extending the one before. Every finite level is itself built by Every natural-number-indexed list of nonempty sets has a choice function on its family of values, a theorem of ZF, so the only place the sequence of levels itself is assembled — rather than any one level — is where DC is spent.

Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a, b]$ extends continuously to the whole space, and this property characterises normality, clause 1, spends dependent choice in the same shape and at the same kind of step: the sequence of approximating pairs $(f_{n}, g_{n})$ , where each $g_{n + 1}$ is chosen using the particular remainder function $f_{n + 1}$ produced from the previous stage. This dependency is genuine — unlike the corresponding step of Under dependent choice a space is perfectly normal if and only if it is normal and every closed set is a zero set below, the relation driving the recursion cannot be replaced by one that ignores its first argument.

The following results on this page assume dependent choice purely by inheritance, through a citation of one of the two results above, and spend no further choice principle of their own: 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, Under dependent choice, a continuous real-valued map on a closed subspace of a normal space extends to the whole space, and a map into an open interval extends into that same open interval, Under dependent choice a locally compact Hausdorff space is completely regular, hence Tychonoff, and Under dependent choice a compact Hausdorff space is Tychonoff, and its disjoint closed sets are separated by continuous functions.

The one place countable choice appears, and why it costs no more than DC

The forward direction of Under dependent choice a space is perfectly normal if and only if it is normal and every closed set is a zero set performs a step shaped like the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )): a Urysohn function is selected for every level of a fixed countable presentation $C = ⋂_{n} U_{n}$ , and the selection at level $n$ does not depend on the one at any other level. That item's own proof discharges this as a direct instance of dependent choice, using a relation that carries no memory of the previous term, so the theorem is stated under DC alone rather than under DC together with a separately-adopted ${A C}_{ω}$ .

Contrast with the choice-free and countable-choice arrows already published

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 proves the metric case of every property this page's headline theorems assert for a general normal space — Urysohn separation, the zero-set characterisation of perfect normality — entirely free of choice, the distance function supplying every function needed by an explicit formula. The contrast confirms that the choice cost on this page belongs to the passage from a topology to no topology beyond normality, not to the properties themselves.

Assuming countable choice, every perfectly normal space is completely normal: separated sets in a normal space whose open sets are all $F_{σ}$ can be separated by disjoint open sets, by contrast, needs only countable choice, and for a structurally different reason than the one above: its single choice-consuming step selects one open set for each member of a countable family of closed sets that already exists in full before any selection is made, with no member of the family depending on an earlier choice. That is the textbook shape of ${A C}_{ω}$ with no disguise needed, unlike the two DC arguments on this page.

What this page does not attempt to show

Nothing here shows dependent choice is necessary for Urysohn's lemma or for Tietze's theorem; that would be an independence result, and this library proves none. What is recorded, with sources, in Urysohn's lemma is not a theorem of ZF, nor of ZF plus countable choice ‡ is that the classical $T_{4}$ form of Urysohn's lemma is a theorem of neither ZF nor ZF together with countable choice, so the DC hypothesis carried by every theorem on this page cannot be weakened to countable choice without leaving the space of what has been established.

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

FALSE: Every normal space is completely regular

Statement

FALSE. Every normal space is completely regular.

This is exactly why 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 carries the hypothesis $T_{1}$ : normality alone, without $T_{1}$ , gives no separation property above itself.

Facts & Assumptions

Given: Sierpinski space $S = {a, b}$ , $a \neq b$ , with topology $T_{S i e r} = {\emptyset, {b}, S}$ (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).

[L1]

The closed sets of $S$ are the complements of $T_{S i e r}$ : $S ∖ \emptyset = S$ , $S ∖ {b} = {a}$ , $S ∖ S = \emptyset$ ; so the closed sets are ${S, {a}, \emptyset}$ (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L2]

$S$ is normal when disjoint closed subsets of $S$ admit disjoint open supersets (Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly).

[L3]

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

[L4]

Every completely regular space is regular (Every completely regular space is regular, and every Tychonoff space is $T_{3}$ , Completely regular spaces and Tychonoff ( $T_{3 \frac{1}{2}}$ ) spaces).

Refutation

technique · constructive

1.1

Let $S = {a, b}$ with $a \neq b$ and $T_{S i e r} = {\emptyset, {b}, S}$ ; by [L1] its closed sets are ${S, {a}, \emptyset}$ .

givenL1construct

2.1

$S$ is normal: let $A, B$ be disjoint closed subsets of $S$ . The nonempty closed sets are ${a}$ and $S$ , and ${a} \subseteq S$ , so any two nonempty closed sets of $S$ meet at $a$ ; hence disjointness of $A, B$ forces $A = \emptyset$ or $B = \emptyset$ . If $A = \emptyset$ , take $U : = \emptyset \supseteq A$ and $V : = S \supseteq B$ ; if $B = \emptyset$ , take $U : = S \supseteq A$ and $V : = \emptyset \supseteq B$ . Either way $U, V$ are open and $U \cap V = \emptyset$ .

step 1.1L1L2algebra

2.2

$S$ is not regular: $b \notin {a}$ , since $a \neq b$ , and ${a}$ is closed by step 1.1. Every open set containing $a$ equals $S$ , since among $\emptyset, {b}, S$ only $S$ contains $a$ ; so any open $V \supseteq {a}$ has $V = S$ , and any open $U ∋ b$ then satisfies $U \cap V = U \cap S = U \neq \emptyset$ , since $b \in U$ . So no disjoint open $U ∋ b$ , $V \supseteq {a}$ exist, and $S$ is not regular.

step 1.1L1L3

3.1

By [L4], complete regularity implies regularity; by step 2.2, $S$ is not regular, so $S$ is not completely regular. With step 2.1, $S$ is a normal space that is not completely regular, refuting the statement.

step 2.1step 2.2L4discharge-construct∎

Remarks

The failure is exactly the missing $T_{1}$ . Sierpinski space is $T_{0}$ (the open set ${b}$ distinguishes $a$ from $b$ ) but not $T_{1}$ : the singleton ${b}$ is not among the closed sets ${S, {a}, \emptyset}$ of step 1.1, so $b$ has no closed singleton. Consequently 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 never claims anything about a normal space that is not $T_{1}$ .
Every disjoint closed pair in $S$ is separated for a trivial reason. Step 2.1 never invokes Urysohn's lemma or any function; normality here has nothing to do with continuous functions, because the only disjoint pairs available involve $\emptyset$ .

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-09-09 (gpt-6-astra)Open item page →

FALSE: Every continuous real-valued function on a subspace of a normal space extends continuously to the whole space

Statement

FALSE. Every continuous real-valued function on a subspace of a normal space extends continuously to the whole space.

The witness isolates the closed-subspace hypothesis in the real-valued form, clause 1 of Under dependent choice, a continuous real-valued map on a closed subspace of a normal space extends to the whole space, and a map into an open interval extends into that same open interval. Even under that corollary's dependent-choice assumption, dropping closedness permits a continuous map with no continuous extension. The nonextension proof below uses no choice principle. The bounded-range version Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a, b]$ extends continuously to the whole space, and this property characterises normality is a different comparison: the reciprocal violates its bounded-range hypothesis as well as closedness.

Facts & Assumptions

Given: $R$ with its usual topology, the subspace $A : = (0, 1] \subseteq R$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, 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), and $f : A \to R$ , $f (x) : = 1 / x$ .

[L1]

$R$ is normal, being metrizable (In a metric space any two separated sets have disjoint open neighbourhoods, so every metrizable space is completely normal).

[L2]

Quotients of continuous real functions with nonvanishing denominator are continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, clause 4); in particular $x \mapsto 1 / x$ is continuous on ${x \in R : x \neq 0} \supseteq A$ .

[L3]

Continuity passes to subsets of the domain: if $B \subseteq C \subseteq R$ and $g : C \to R$ is continuous, then $g ∣_{B}$ is continuous (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

[L4]

$[0, 1]$ is compact (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact).

[L5]

A continuous real function on a compact subset $K$ of its domain is bounded on $K$ : there is real $M \geq 0$ with $∣ g (x) ∣ \leq M$ for every $x \in K$ (A continuous real function on a compact subset of $R$ is bounded).

[L6]

For every real $ε > 0$ there is a natural $n \geq 1$ with $1 / n < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Refutation

technique · contradiction

1.1

$f$ is continuous on $A$ , by [L2] with $0 \notin A$ ; and $R$ is normal, by [L1].

givenL1L2

1.2

For every real $M$ , there is $x \in A$ with $f (x) > M$ : if $M \leq 0$ , take $x : = 1$ , so $f (1) = 1 > 0 \geq M$ ; if $M > 0$ , [L6] applied to $ε : = 1 / (M + 1) > 0$ gives a natural $n \geq 1$ with $1 / n < 1 / (M + 1)$ , hence $n > M + 1 > M$ ; taking $x : = 1 / n \in (0, 1] = A$ gives $f (x) = 1 / x = n > M$ .

givenL6algebrachoose

1.3

Suppose, toward a contradiction, that a continuous $F : R \to R$ exists with $F ∣_{A} = f$ .

assume-contra

1.4

$[0, 1]$ is compact, by [L4].

2.1

Under step 1.3: $F ∣_{[0, 1]}$ is continuous, by [L3] applied to $F$ on $R \supseteq [0, 1]$ .

step 1.3L3

3.1

Under step 1.3: by [L5] applied to $F ∣_{[0, 1]}$ (step 2.1) and $K : = [0, 1]$ (step 1.4), fix a real $M_{0} \geq 0$ with $∣ F (x) ∣ \leq M_{0}$ for every $x \in [0, 1]$ .

step 2.1step 1.4L5choose

4.1

Under step 1.3: for $x \in A$ , $F (x) = f (x)$ (step 1.3) and $x \in [0, 1]$ , so $f (x) \leq ∣ F (x) ∣ \leq M_{0}$ by step 3.1; but step 1.2 applied with $M : = M_{0}$ gives $x_{0} \in A$ with $f (x_{0}) > M_{0}$ , contradicting $f (x_{0}) \leq M_{0}$ .

step 1.3step 3.1step 1.2discharge-contradiction∎

Remarks

Closedness is isolated in the real-valued form. $R$ is normal and $f$ is continuous on $A$ (step 1.1), but $A$ is not closed: its closure is $[0, 1]$ . Thus, even assuming dependent choice, the witness meets every hypothesis of clause 1 of Under dependent choice, a continuous real-valued map on a closed subspace of a normal space extends to the whole space, and a map into an open interval extends into that same open interval except closedness. It does not isolate closedness in Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a, b]$ extends continuously to the whole space, and this property characterises normality, since step 1.2 also rules out any bounded interval containing its range.
The obstruction is unboundedness near the missing point, not discontinuity. $f$ itself is continuous at every point of its own domain $A$ ; nothing about $f$ is badly behaved on $A$ . What blocks an extension is that $f$ has no finite value it could sensibly take at the boundary point $0 \notin A$ , and step 1.2 makes that failure of boundedness explicit rather than appealing to a limit that does not exist.

Urysohn's Lemma and the Tietze Extension Theorem

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

The dyadic rationals of [0,1][0,1], their finite levels DnDn​, and their density in [0,1][0,1]

Definition

Remarks

If (Ur)r∈D(Ur​)r∈D​ are open with Ur‾⊆UsUr​​⊆Us​ whenever r<sr<s and U1=XU1​=X, then x↦inf⁡{r∈D:x∈Ur}x↦inf{r∈D:x∈Ur​} is a continuous map X→[0,1]X→[0,1], and no choice principle is used

Statement

Facts & Assumptions

Proof

Remarks

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][0,1], and conversely such a space is normal

Statement

Facts & Assumptions

Proof

Remarks

Under dependent choice a normal T1T1​ space is completely regular, so T4⇒T312T4​⇒T321​​, and together with the implications already proved this is the whole classical chain

Statement

Facts & Assumptions

Proof

Remarks

If for every ε>0ε>0 some continuous g:X→Rg:X→R satisfies ∣f(x)−g(x)∣<ε∣f(x)−g(x)∣<ε for all xx, then ff is continuous; in particular a uniformly convergent series of continuous real functions has a continuous sum

Statement

Facts & Assumptions

Proof

Remarks

Under dependent choice a space is perfectly normal if and only if it is normal and every closed set is a zero set

Statement

Facts & Assumptions

Proof

Remarks

Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into [a,b][a,b] extends continuously to the whole space, and this property characterises normality

Statement

Facts & Assumptions

Proof

Remarks

Under dependent choice, a continuous real-valued map on a closed subspace of a normal space extends to the whole space, and a map into an open interval extends into that same open interval

Statement

Facts & Assumptions

Proof

Remarks

Under dependent choice a locally compact Hausdorff space is completely regular, hence Tychonoff

Statement

Facts & Assumptions

Proof

Remarks

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

Statement

Facts & Assumptions

Proof

Remarks

Which results on this page spend dependent choice, which spend countable choice, and which are theorems of ZF

What is proved free of any choice principle

What spends dependent choice, and at which single step

The one place countable choice appears, and why it costs no more than DC

Contrast with the choice-free and countable-choice arrows already published

What this page does not attempt to show

5 · Examples, counterexamples and false statements

FALSE: Every normal space is completely regular

Statement

Facts & Assumptions

Refutation

Remarks

FALSE: Every continuous real-valued function on a subspace of a normal space extends continuously to the whole space

Statement

Facts & Assumptions

Refutation

Remarks

Sources

The dyadic rationals of $[0, 1]$ , their finite levels $D_{n}$ , and their density in $[0, 1]$

If $(U_{r})_{r \in D}$ are open with $\overline{U_{r}} \subseteq U_{s}$ whenever $r < s$ and $U_{1} = X$ , then $x \mapsto \inf {r \in D : x \in U_{r}}$ is a continuous map $X \to [0, 1]$ , and no choice principle is used

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

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

If for every $ε > 0$ some continuous $g : X \to R$ satisfies $∣ f (x) - g (x) ∣ < ε$ for all $x$ , then $f$ is continuous; in particular a uniformly convergent series of continuous real functions has a continuous sum

Tietze's extension theorem, under dependent choice: a continuous map from a closed subspace of a normal space into $[a, b]$ extends continuously to the whole space, and this property characterises normality