LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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 $\mathbb{R}^n$ , the straight-line formula defines a continuous homotopy

Statement

Let $n\ge1$ . A subset $C\subseteq\mathbb R^n$ is called convex here when

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

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

$H:X\times I\longrightarrow C,\qquad H(x,t)=(1-t)f(x)+tg(x),$

is continuous.

Facts & Assumptions

Given: A natural $n\ge1$ , a convex subspace $C\subseteq\mathbb 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 $\mathbb R^m$ agrees with its Euclidean metric topology for every $m\ge1$ (For $n \ge 1$ the product topology on $n$ copies of the usual topology of $\mathbb{R}$ is the metric topology of $d_\infty$ on $\mathbb{R}^n$ , and hence also of $d_1$ and $d_2$ , so $\mathbb{R}^n$ as a product and $\mathbb{R}^n$ as a metric space are one space).

[L3]

For maps from a metric space into $\mathbb 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 $\mathbb R^2\to\mathbb 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 $\mathbb 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_0z_1$ is continuous by its algebra part.

L1L2L3

2.1

Consequently, if $a,b:Z\to\mathbb R$ are continuous on an arbitrary topological space $Z$ , then $a+b$ and $ab$ are continuous: the pair $(a,b):Z\to\mathbb 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 $\iota:C\hookrightarrow\mathbb R^n$ be the inclusion and put $F=\iota\circ f$ , $G=\iota\circ g$ . These ambient maps are continuous by [L4]. For $Z=X\times I$ , let $p_X:Z\to X$ and $\tau:Z\to I\subseteq\mathbb R$ be the projections. Each scalar coordinate $F_k\circ p_X$ and $G_k\circ p_X$ is continuous: coordinate projections on $\mathbb R^n$ are continuous by [L1] and [L2], and composites preserve continuity by the preimage calculation of step 2.1. The scalar map $\tau$ is continuous, also as a map into $\mathbb 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)+tG_k(x)$ is continuous on $Z$ . Therefore the ambient map $\widetilde H:Z\to\mathbb R^n$ with these coordinates is continuous by [L1] and [L2].

step 2.1step 3.1L1L2

5.1

Convexity [A1] gives $\widetilde H(x,t)\in C$ for every $(x,t)\in Z$ . Since the composite of $H:Z\to C$ with the inclusion $\iota$ is $\widetilde 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 137 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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

For continuous maps into a convex subset of Rn\mathbb{R}^nRn, the straight-line formula defines a continuous homotopy