Every plane face is incident with a dart

Proved

EveryFaceIncidentDart

by xuanji · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theoryplanar-graphs

Let $G$ be a connected finite simple graph with at least three vertices and at least one edge, and let $D$ be a crossing-free ordinary polygonal drawing with plane face data $A$ . Then every face $F$ of $A$ is the left face of some dart: there exists a dart $d$ with $A.leftFace\,d=F$ .

Preamble

import Definitions.Def_PlaneFaceData
import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

open Classical
noncomputable section

Formal statement

lemma EveryFaceIncidentDart {V : Type*} [Fintype V] (G : SimpleGraph V)
    [Fintype G.edgeSet] [DecidableRel G.Adj] (D : OrdinaryPolygonalDrawing G)
    (hD : D.crossingSet.card = 0) (A : PlaneFaceData G D) :
    G.Connected → 3 ≤ Fintype.card V → 0 < G.edgeFinset.card →
      ∀ F : A.Face, ∃ d : G.Dart, A.leftFace d = F := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/EveryFaceIncidentDart.lean#L1-L24

View graph