TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03

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.

Every nonempty convex subset of $R^{n}$ is simply connected

Statement

Let $n \geq 1$ and let $C \subseteq R^{n}$ be nonempty and convex, with its Euclidean subspace topology. Then $C$ is simply connected. More explicitly, for every basepoint $x_{0} \in C$ and every loop $α$ at $x_{0}$ , the formula

$H (s, t) = (1 - t) α (s) + t x_{0}$

is a path homotopy relative to the endpoints from $α$ to the constant loop at $x_{0}$ .

Facts & Assumptions

Given: A nonempty convex subset $C \subseteq R^{n}$ , a basepoint $x_{0} \in C$ , and a based loop $α : I \to C$ .

[L1]

The straight-line formula between two continuous maps into a convex subset is a continuous homotopy (For continuous maps into a convex subset of $R^{n}$ , the straight-line formula defines a continuous homotopy).

[L2]

Every nonempty contractible space is path-connected, and the published straight-line contraction makes a nonempty convex subset contractible (Every nonempty contractible space is path-connected and its dependency Every nonempty convex subset of $R^{n}$ is contractible).

[L3]

A loop class is the identity exactly when the loop is endpoint-homotopic to the constant loop (Based loops and the fundamental group, Loop classes form the group $π_{1} (X, x_{0})$ under concatenation).

[L4]

Simple connectedness means nonempty path-connectedness and a one-element fundamental group at every basepoint (Simply connected topological spaces).

Proof

technique · direct

1.1

Apply [L1] to the maps $α : I \to C$ and $c_{x_{0}} : I \to C$ ; it gives the displayed continuous homotopy $H (s, t) = (1 - t) α (s) + t x_{0}$ .

2.1

Since $α (0) = α (1) = x_{0}$ , one has $H (0, t) = x_{0} = H (1, t)$ for every $t$ , so this homotopy is relative to the endpoints.

step 1.1L3

3.1

Steps 1.1 and 2.1 show that every loop at every basepoint represents the constant-loop class, so each fundamental group has one element; [L2] supplies nonempty path-connectedness.

step 1.1step 2.1L2L3

4.1

Therefore $C$ is simply connected by [L4].

step 3.1L4∎

Depends on

Used by

Dependency tree · two levels

20 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

A. Hatcher, Algebraic Topology, Chapter 1, Example 1.4 (standard reference, not scraped)

Every nonempty convex subset of RnRn is simply connected