A plane tree has one face

Open

PlaneTreeOneFace

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

graph-theoryplanar-graphs

Let $G$ be a finite simple graph with finite edge set and decidable adjacency, let $D$ be an ordinary polygonal drawing of $G$ with no crossings, and let $A$ be plane-face data for $G$ and $D$ . If $G$ is a tree, then the face type carried by $A$ has exactly one element:

\#\,A.\mathrm{Face}=1.

Thus a crossing-free drawing of a tree has a single complementary face in the plane-face decomposition.

Preamble

import Definitions.Def_PlaneFaceData
import Mathlib.Combinatorics.SimpleGraph.Acyclic

open Classical
noncomputable section

-- [TABLET NODE: PlaneTreeOneFace]

Formal statement

lemma PlaneTreeOneFace {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.IsTree → @Fintype.card A.Face A.faceFintype = 1 := by sorry

Source

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

View graph