LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31

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.

A finite concatenation of straight segments in $\mathbb{R}^n$ is a continuous path

Statement

Let $v_0,\ldots,v_m\in\mathbb{R}^n$ and $0=t_0<\cdots<t_m=1$ . The affine pieces joining $v_{i-1}$ to $v_i$ define a continuous map $[0,1]\to\mathbb{R}^n$ . If every piece lies in a subset $A$ , the map is a polygonal path (Polygonal paths and polygonally connected subsets of $\mathbb{R}^n$ ) in $A$ from $v_0$ to $v_m$ .

Facts & Assumptions

Given: Vertices $v_0,\ldots,v_m\in\mathbb{R}^n$ and a partition $0=t_0<\cdots<t_m=1$ .

[L1]

A finite family of closed sets covering a space pastes continuous restrictions to a continuous map (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, claim 3).

[L2]

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

[L3]

A map into $\mathbb{R}^n$ is continuous if and only if all of its coordinate functions 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, clause 1).

Proof

technique · constructive

1.1

On $[t_{i-1},t_i]$ define $\gamma_i(t):=((t_i-t)/(t_i-t_{i-1}))v_{i-1}+((t-t_{i-1})/(t_i-t_{i-1}))v_i$ . Each coordinate is an affine real function of $t$ , hence continuous.

L3construct

2.1

At every shared endpoint $t_i$ , the adjacent formulas both give $v_i$ , so the pieces define one function $\gamma:[0,1]\to\mathbb{R}^n$ .

step 1.1construct

3.1

Each interval $[t_{i-1},t_i]$ is closed in $[0,1]$ , the finitely many intervals cover it, and each restriction of $\gamma$ is continuous by step 1.1. Thus $\gamma$ is continuous by [L1].

L1step 1.1step 2.1

4.1

If the pieces lie in $A$ , then $\gamma$ takes values in $A$ . Its composite with the inclusion $A\hookrightarrow\mathbb R^n$ is the continuous map of step 3.1, so [L2] makes it continuous into the subspace $A$ . Its endpoints are $v_0,v_m$ , hence it is a path in $A$ .

step 3.1L2discharge-construct∎

Depends on

Used by

Dependency tree · next 3 levels

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

Path-connected space (standard reference, not scraped)
Pasting lemma (Wikipedia) (standard reference, not scraped)
Polygonal chain (standard reference, not scraped)

A finite concatenation of straight segments in Rn\mathbb{R}^nRn is a continuous path