Existence of an ordinary polygonal drawing
ProvedOrdinaryPolygonalDrawingNonemptycrossing-numbergeometrygraph-theory
Every finite simple graph admits at least one ordinary polygonal drawing:
The result provides the nonemptiness needed to take a minimum over drawing crossing sets. It is a structural existence statement, independent of any crossing-number bound.
Preamble
import Definitions.Def_OrdinaryPolygonalDrawing open Classical noncomputable section
Formal statement
lemma OrdinaryPolygonalDrawingNonempty {V : Type*} [Fintype V] (G : SimpleGraph V)
[Fintype G.edgeSet] :
Nonempty (OrdinaryPolygonalDrawing G) := by sorrySource