LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-07-31verified 2026-08-08 (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.

For continuous maps into a convex subset of $R^{n}$ , the straight-line formula defines a continuous homotopy

Statement

Let $n \geq 1$ . A subset $C \subseteq R^{n}$ is called convex here when

$u, v \in C, t \in [0, 1] ⟹ (1 - t) u + t v \in C .$

If $X$ is a topological space and $f, g : X \to C$ are continuous, where $C$ has the subspace topology from $R^{n}$ , then

$H : X \times I ⟶ C, H (x, t) = (1 - t) f (x) + t g (x),$

is continuous.

Facts & Assumptions

Given: A natural $n \geq 1$ , a convex subspace $C \subseteq R^{n}$ , a topological space $X$ , and continuous maps $f, g : X \to C$ .

[A1]

Convexity is the displayed condition in the Statement.

[L1]

Product projections are continuous, and a map into a product is continuous exactly when all component maps are continuous (A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice).

[L2]

The product topology on $R^{m}$ agrees with its Euclidean metric topology for every $m \geq 1$ (For $n \geq 1$ the product topology on $n$ copies of the usual topology of $R$ is the metric topology of $d_{\infty}$ on $R^{n}$ , and hence also of $d_{1}$ and $d_{2}$ , so $R^{n}$ as a product and $R^{n}$ as a metric space are one space).

[L3]

For maps from a metric space into $R^{m}$ , continuity is componentwise; sums and scalar multiples of continuous vector-valued maps and inner products of two such maps are continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, clauses 1 and 3).

[L4]

A map into a subspace is continuous exactly when its composite with the ambient inclusion 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).

[L5]

A map is continuous exactly when preimages of open sets 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)}$ , condition (b)).

Proof

technique · direct

1.1

Addition and multiplication $R^{2} \to R$ are continuous. Indeed the coordinate projections are continuous by [L1], and by [L2] may be read as continuous scalar functions on the Euclidean metric space $R^{2}$ . The identity map $z \mapsto z$ and the constant map $z \mapsto (1, 1)$ are continuous, so [L3] makes their inner product $z_{0} + z_{1}$ continuous. The maps $z \mapsto (z_{0}, 0)$ and $z \mapsto (z_{1}, 0)$ are continuous by the componentwise part of [L3], and their inner product $z_{0} z_{1}$ is continuous by its algebra part.

L1L2L3

2.1

Consequently, if $a, b : Z \to R$ are continuous on an arbitrary topological space $Z$ , then $a + b$ and $a b$ are continuous: the pair $(a, b) : Z \to R^{2}$ is continuous by [L1] and [L2], and composing it with the two maps of step 1.1 is continuous because the preimage of an open set under a composite is an iterated preimage, which is open by [L5]. Constant functions and additive inverses are continuous by the same argument, using a constant component and the continuous scalar multiple supplied by [L3].

step 1.1L1L2L3L5

3.1

Let $ι : C ↪ R^{n}$ be the inclusion and put $F = ι \circ f$ , $G = ι \circ g$ . These ambient maps are continuous by [L4]. For $Z = X \times I$ , let $p_{X} : Z \to X$ and $τ : Z \to I \subseteq R$ be the projections. Each scalar coordinate $F_{k} \circ p_{X}$ and $G_{k} \circ p_{X}$ is continuous: coordinate projections on $R^{n}$ are continuous by [L1] and [L2], and composites preserve continuity by the preimage calculation of step 2.1. The scalar map $τ$ is continuous, also as a map into $R$ , by [L1] and [L4].

L1L2L4L5

4.1

By step 2.1, for every $k < n$ the function $(x, t) \mapsto (1 - t) F_{k} (x) + t G_{k} (x)$ is continuous on $Z$ . Therefore the ambient map $\tilde{H} : Z \to R^{n}$ with these coordinates is continuous by [L1] and [L2].

step 2.1step 3.1L1L2

5.1

Convexity [A1] gives $\tilde{H} (x, t) \in C$ for every $(x, t) \in Z$ . Since the composite of $H : Z \to C$ with the inclusion $ι$ is $\tilde{H}$ , [L4] makes $H$ continuous into $C$ .

step 4.1A1L4∎

Remarks

The continuity argument uses only products, subspaces and ordinary Euclidean continuity. Convexity is used solely to ensure that the straight-line formula takes values in $C$ .

Depends on

Used by

Dependency tree · two levels

52 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

Algebraic Topology lecture notes (UC Riverside) (standard reference, not scraped)

For continuous maps into a convex subset of RnRn, the straight-line formula defines a continuous homotopy