Deleting edges from an ordinary polygonal drawing

Proved

OrdinaryPolygonalDrawingDeleteEdges

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

crossing-numbergraph-theory

Let $G$ be a finite simple graph, let $D$ be an ordinary polygonal drawing of $G$ , and let $S$ be a finite set of unordered vertex pairs. After deleting from $G$ every edge whose unordered pair lies in $S$ , there is an ordinary polygonal drawing $D'$ of the resulting graph such that

D'.\operatorname{crossingSet} =\{p\in D.\operatorname{crossingSet}: ext{the crossing at }p ext{ is supported by two retained edges}\},

where the retained-edge condition is expressed by the displayed Lean filter over the original edge finset. Moreover, the new edge count is

|E(G\setminus S)|=|E(G)|-|S\cap E(G)|.

This interface formalizes the operation of deleting a prescribed collection of edges while retaining the original drawing data and exactly the crossings that remain supported by undeleted edges.

Formalization Note Unordered edges are represented by Sym2 V, and the retained crossing condition is stated using the original edge finset of $G$ .

Preamble

import Definitions.Def_OrdinaryPolygonalDrawing
import Mathlib.Combinatorics.SimpleGraph.Copy

open Classical
noncomputable section

Formal statement

lemma OrdinaryPolygonalDrawingDeleteEdges {V : Type*} [Fintype V] (G : SimpleGraph V)
    [Fintype G.edgeSet] (D : OrdinaryPolygonalDrawing G)
    (S : Finset (Sym2 V)) :
    ∃ D' : OrdinaryPolygonalDrawing (G.deleteEdges (S : Set (Sym2 V))),
      D'.crossingSet =
          D.crossingSet.filter (fun p =>
            ∃ e₁ e₂ : G.edgeFinset,
              e₁ ≠ e₂ ∧ e₁.1 ∉ S ∧ e₂.1 ∉ S ∧
                p ∈ (D.edgeArc e₁).relativeInterior ∧
                  p ∈ (D.edgeArc e₂).relativeInterior) ∧
        (G.deleteEdges (S : Set (Sym2 V))).edgeFinset.card =
          G.edgeFinset.card - (S ∩ G.edgeFinset).card := by sorry

Source

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

View graph