TheoremStatement: Literature-sourcedProof: AI-adaptedSession-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.

Any two continuous maps into a nonempty convex subset of $\mathbb{R}^n$ are homotopic by straight lines

Statement

Let $n\ge1$ , let $C\subseteq\mathbb R^n$ be nonempty and convex in the sense stated in For continuous maps into a convex subset of $\mathbb{R}^n$ , the straight-line formula defines a continuous homotopy, and let $f,g:X\to C$ be continuous. Then

$H(x,t)=(1-t)f(x)+tg(x)$

is a homotopy from $f$ to $g$ .

Facts & Assumptions

Given: A nonempty convex $C\subseteq\mathbb R^n$ with $n\ge1$ and continuous maps $f,g:X\to C$ .

[L1]

The straight-line formula defines a continuous map $H:X\times I\to C$ (For continuous maps into a convex subset of $\mathbb{R}^n$ , the straight-line formula defines a continuous homotopy).

[A1]

A homotopy from $f$ to $g$ is a continuous $H:X\times I\to C$ with $H(x,0)=f(x)$ and $H(x,1)=g(x)$ (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).

Proof

technique · direct

1.1

The map $H(x,t)=(1-t)f(x)+tg(x)$ is continuous by [L1].

1.2

Substitution gives $H(x,0)=f(x)$ and $H(x,1)=g(x)$ for every $x\in X$ .

algebra

2.1

Thus $H$ satisfies the continuity and endpoint conditions of [A1], so it is a homotopy from $f$ to $g$ .

step 1.1step 1.2A1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 64 results over 16 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)

Any two continuous maps into a nonempty convex subset of Rn\mathbb{R}^nRn are homotopic by straight lines