Compactness of an ordinary polygonal drawing image
ProvedOrdinaryDrawingImageCompactFor a finite graph with an ordinary polygonal drawing, the drawing image—the finite set of vertex locations together with the finitely many polygonal edge carriers—is compact in the Euclidean plane.
This compactness supplies a boundedness witness for choosing a point outside the drawing image.
Preamble
import Definitions.Def_PlaneFaceData open Classical noncomputable section -- [TABLET NODE: OrdinaryDrawingImageCompact]
Formal statement
lemma OrdinaryDrawingImageCompact {V : Type*} [Fintype V] (G : SimpleGraph V)
[Fintype G.edgeSet] (D : OrdinaryPolygonalDrawing G) :
IsCompact (OrdinaryDrawingImage G D) := by sorrySource