Euler formula for connected plane drawings

Open

ConnectedEulerFormula

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

For a connected finite graph with a crossing-free ordinary polygonal drawing, the numbers of vertices, edges, and indexed faces satisfy the Euler relation n minus e plus f equals 2.

Preamble

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

open Classical
noncomputable section

Formal statement

lemma ConnectedEulerFormula {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 →
      (Fintype.card V : ℤ) - (G.edgeFinset.card : ℤ) +
        (@Fintype.card A.Face A.faceFintype : ℤ) = 2 := by sorry

Source

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

View graph