Distinct edge interiors are disjoint in a crossing-free drawing

Proved

CrossingFreeEdgeInteriorDisjoint

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

geometrygraph-theoryplanar-graphs

Let $G$ be a finite simple graph equipped with an ordinary polygonal drawing $D$ . If the drawing has no crossing points, then the relative interiors of any two distinct drawn edges are disjoint. In other words, for distinct edges $e_1$ and $e_2$ and any point $p$ ,

e_1\ne e_2 \quad\Longrightarrow\quad p\in\operatorname{relint}(D(e_1))\ \text{and}\ p\in\operatorname{relint}(D(e_2))\ \text{is impossible}.

This is the basic crossing-free separation fact used when analyzing how a pendant edge can meet the remainder of a planar drawing.

Formalization Note The drawing's crossing set is a finite set of points, and the hypothesis that its cardinality is zero expresses that it is empty.

Preamble

import Definitions.Def_OrdinaryPolygonalDrawing

open Classical
noncomputable section

Formal statement

lemma CrossingFreeEdgeInteriorDisjoint {V : Type*} [Fintype V]
    (G : SimpleGraph V) [Fintype G.edgeSet]
    (D : OrdinaryPolygonalDrawing G) (hD : D.crossingSet.card = 0) :
    ∀ ⦃e₁ e₂ : G.edgeFinset⦄ ⦃p : EuclideanSpace ℝ (Fin 2)⦄,
      e₁ ≠ e₂ →
        p ∈ (D.edgeArc e₁).relativeInterior →
          p ∈ (D.edgeArc e₂).relativeInterior → False := by sorry

Source

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

View graph