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

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Under dependent choice a 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]

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]

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.

Depends on

Used by

Dependency tree · two levels

82 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Perfectly normal space (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §33, Exercise 6 (standard reference, not scraped)