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

Depends on

Used by

Dependency tree · two levels

87 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)