Polygonal path connectedness
DefinitionPolygonallyPathConnectedA subset of the plane is polygonally path connected when every pair of its points can be joined by a polygonal path whose source and target are those points and whose entire carrier remains inside the subset. This predicate is the connectivity interface used for complements of planar drawings.
Definition code
import Definitions.Def_PolygonalPath
-- [TABLET NODE: PolygonallyPathConnected]
def PolygonallyPathConnected (S : Set (EuclideanSpace ℝ (Fin 2))) : Prop :=
-- BODY
∀ ⦃p q : EuclideanSpace ℝ (Fin 2)⦄,
p ∈ S → q ∈ S →
∃ γ : PolygonalPath,
γ.source = p ∧ γ.target = q ∧ γ.carrier ⊆ S
Source