A polygonally path-connected drawing complement has one face

Proved

PlaneFaceDataOneFaceOfPolygonallyPathConnectedComplement

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

Let $G$ be a finite simple graph with an ordinary polygonal drawing $D$ , and let $A$ be plane-face data for that drawing. If the complement of the drawing image is polygonally path connected and nonempty, then every face component is the whole complement, so the face type has exactly one element:

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

This is the topological bridge from polygonal path connectedness of a planar drawing's complement to uniqueness of its face.

Preamble

import Definitions.Def_PlaneFaceData
import Definitions.Def_PolygonallyPathConnected

open Classical
noncomputable section

-- [TABLET NODE: PlaneFaceDataOneFaceOfPolygonallyPathConnectedComplement]

Formal statement

lemma PlaneFaceDataOneFaceOfPolygonallyPathConnectedComplement {V : Type*}
    [Fintype V] (G : SimpleGraph V) [Fintype G.edgeSet]
    [DecidableRel G.Adj] (D : OrdinaryPolygonalDrawing G)
    (A : PlaneFaceData G D) :
    PolygonallyPathConnected ((OrdinaryDrawingImage G D)ᶜ) →
      ((OrdinaryDrawingImage G D)ᶜ).Nonempty →
        @Fintype.card A.Face A.faceFintype = 1 := by sorry

Source

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

View graph