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 , the punctured space is polygonally connected
Statement
For , is polygonally connected.
Facts & Assumptions
Given: and nonzero vectors .
The standard unit vectors form a basis of , so a one-dimensional span is a proper subspace when (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension , Linear combination of a finite list, and the span as the smallest linear subspace containing ).
A vector outside cannot lie on a segment from to , except at no point; the corresponding statement holds for , by the vector-space axioms (Linear combination of a finite list, and the span as the smallest linear subspace containing , A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).
A finite concatenation of segments contained in a subset is a polygonal path in that subset (A finite concatenation of straight segments in is a continuous path).
Proof
Choose . Such a vector exists: if the two spans differ, lies in neither; if they agree, [L1] gives a vector outside their common proper subspace.
The segment from to avoids : an equality with would give , contrary to step 1.1. The segment from to similarly avoids .
The two segments therefore form a polygonal path in from to by [L3].
Since were arbitrary nonzero vectors, the punctured space is polygonally connected.
Depends on
- Polygonal paths and polygonally connected subsets of $\mathbb{R}^n$
- A finite concatenation of straight segments in $\mathbb{R}^n$ is a continuous path
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
- Linear combination of a finite list, and the span $\operatorname{span}(S)$ as the smallest linear subspace containing $S$
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
Used by
- For n≥2, the sphere Sⁿ⁻¹ is path-connected and connected Corollary
- A connected complex domain need not be star-shaped Counterexample
- Agreement accumulating only at the boundary does not force a holomorphic identity Counterexample
- GL₁(ℝ)=ℝ∖{0} is disconnected, whereas ℝ²∖{0} is polygonally connected Example
- FALSE: every continuous complex-valued function on a domain has a primitive False statement
- Antipodal complements cover Sⁿ by simply connected sets with path-connected overlap for n≥2 Lemma
- ℝ is not homeomorphic to ℝⁿ for any n≥2 Theorem
Dependency tree · two levels
42 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
- Path-connected space (standard reference, not scraped)
- Euclidean space (Wikipedia) (standard reference, not scraped)