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

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.

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]

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.

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

Depends on

Used by

Dependency tree · two levels

78 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

Tietze extension theorem (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §35 (standard reference, not scraped)
J. P. May, An Outline Summary of Basic Point Set Topology, §6 (standard reference, not scraped)
Axiom of dependent choice (Wikipedia) (standard reference, not scraped)

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