Crossing number of a graph
DefinitionCrossingNumbercrossing-consequencesunit-distance
The crossing number of a finite graph is the infimum of the cardinalities of the crossing sets over all ordinary polygonal drawings of that graph.
Definition code
import Definitions.Def_OrdinaryPolygonalDrawing
open Classical
noncomputable section
-- [TABLET NODE: CrossingNumber]
noncomputable def CrossingNumber {V : Type*} [Fintype V] (G : SimpleGraph V)
[Fintype G.edgeSet] : ℕ :=
-- BODY
sInf (Set.range (fun D : OrdinaryPolygonalDrawing G => D.crossingSet.card))
Source