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.
The complement of a polygonal arc in is polygonally connected
Statement
If is a polygonal arc (Polygonal arcs and polygons as non-self-intersecting finite unions of line segments in ), then is polygonally connected and therefore has one region in the sense of Regions of the complement of a planar set and their frontiers. The completion step uses the finite general-position argument of Every point off a polygon admits a ray meeting it transversely in finitely many nonvertex points, followed by Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each and the ambient polygonal connectedness supplied by Every connected component of an open subset of is open and polygonally connected.
Facts & Assumptions
Given: A polygonal arc and points .
A polygonal path is specified by a finite list of vertices and is a path in the ambient subset (Polygonal paths and polygonally connected subsets of ).
A polygon has exactly two complementary regions, each with the polygon as frontier (Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each).
Proof
Complete to a polygon , where is a polygonal arc with the same endpoints as , has no other point in common with , and avoids . To construct , take a sufficiently thin polygonal regular neighbourhood of the finite arc : disjoint small vertex neighbourhoods joined by narrow strips along the edge interiors form a polygonal disk, and either boundary chain, capped to the two endpoints, supplies . General position permits the finitely many boundary vertices to avoid .
By [L1], has regions and . If lie in the same region, polygonal connectedness of open components joins them there. If they lie in opposite regions, choose a point in the relative interior of . A sufficiently short segment transverse to at has one endpoint in and the other in . Join to the endpoint on its side and to the other by polygonal paths within those regions, then concatenate those paths with .
The paths in step 2.1 avoid all of except possibly at , and consists only of the two common endpoints, so the concatenated path avoids . Since were arbitrary, is polygonally connected.
Depends on
- Polygonal arcs and polygons as non-self-intersecting finite unions of line segments in $\mathbb R^2$
- Every point off a polygon admits a ray meeting it transversely in finitely many nonvertex points
- Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each
- Every connected component of an open subset of $\mathbb{R}^n$ is open and polygonally connected
- Regions of the complement of a planar set and their frontiers
- Polygonal paths and polygonally connected subsets of $\mathbb{R}^n$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 100 results over 18 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
- R. Diestel, Graph Theory, 6th ed., Lemma 4.1.3 (standard reference, not scraped)