OpenConnectedComponentPolygonallyConnected
ProvedOpenConnectedComponentPolygonallyConnectedcrossing-consequencesgeometrypolygonal
Every connected component of the complement of an open set in the Euclidean plane is polygonally path connected: any two points in the component can be joined by a polygonal path contained in that component.
Preamble
import Definitions.Def_ComplementComponent import Definitions.Def_PolygonallyPathConnected
Formal statement
lemma OpenConnectedComponentPolygonallyConnected
(U C : Set (EuclideanSpace ℝ (Fin 2))) :
IsOpen U → ComplementComponent Uᶜ C → PolygonallyPathConnected C := by sorrySource