Induced-subgraph drawing bridge
ProvedInducedSubdrawingBridgecrossing-numbergeometrygraph-theory
Given an ordinary polygonal drawing of a finite simple graph and a vertex subset , one can draw the induced graph by restricting the vertex placement and retaining exactly the edges whose endpoints lie in .
The bridge identifies every induced edge with its original edge, characterizes the induced crossing set by crossings of retained original edges, and shows that a drawing with no adjacent-edge crossings has no common endpoint between any two edges crossing in their relative interiors. These correspondences let crossing-number inequalities for induced subgraphs be compared with the original drawing.
Preamble
import Definitions.Def_OrdinaryPolygonalDrawing import Mathlib.Combinatorics.SimpleGraph.Copy set_option maxHeartbeats 1000000 open Classical noncomputable section
Formal statement
lemma InducedSubdrawingBridge {V : Type*} [Fintype V] (G : SimpleGraph V)
[Fintype G.edgeSet] (D : OrdinaryPolygonalDrawing G) (S : Set V)
[Fintype S] [Fintype (G.induce S).edgeSet] :
∃ DX : OrdinaryPolygonalDrawing (G.induce S),
DX.vertexPlacement = (fun v : S => D.vertexPlacement v.1) ∧
(∀ ed : (G.induce S).edgeFinset,
∃ eG : G.edgeFinset,
eG.1 = Sym2.map (Subtype.val : S → V) ed.1 ∧
(∀ v : V, v ∈ eG.1 → v ∈ S) ∧
DX.edgeArc ed = D.edgeArc eG) ∧
(∀ p : EuclideanSpace ℝ (Fin 2),
p ∈ DX.crossingSet ↔
∃ e₁ e₂ : G.edgeFinset,
e₁ ≠ e₂ ∧
(∀ v : V, v ∈ e₁.1 → v ∈ S) ∧
(∀ v : V, v ∈ e₂.1 → v ∈ S) ∧
p ∈ (D.edgeArc e₁).relativeInterior ∧
p ∈ (D.edgeArc e₂).relativeInterior) ∧
(D.adjacentEdgeCrossingCount = 0 →
∀ ⦃p : EuclideanSpace ℝ (Fin 2)⦄ ⦃e₁ e₂ : G.edgeFinset⦄,
e₁ ≠ e₂ →
p ∈ (D.edgeArc e₁).relativeInterior →
p ∈ (D.edgeArc e₂).relativeInterior →
¬ ∃ v : V, v ∈ e₁.1 ∧ v ∈ e₂.1) := by sorrySource