Existence of plane face data
OpenPlaneFaceDataExistsEvery crossing-free ordinary polygonal drawing of a finite simple graph admits a plane face data record carrying the indexed faces and the associated dart, side-strip, sector, and cyclic successor information.
Preamble
import Definitions.Def_PlaneFaceData open Classical noncomputable section
Formal statement
lemma PlaneFaceDataExists {V : Type*} [Fintype V] (G : SimpleGraph V)
[Fintype G.edgeSet] [DecidableRel G.Adj] (D : OrdinaryPolygonalDrawing G)
(hD : D.crossingSet.card = 0) :
Nonempty (PlaneFaceData G D) := by sorrySource