The underlying simple graph of a CFGraph

underlyingSimpleGraph and the equivalence between the cut definition of connectivity and SimpleGraph.Connected. This provides a general interface from chip-firing multigraphs to Mathlib's simple-graph connectivity theory.

def Utilities.underlyingSimpleGraph (G : CFGraph) : SimpleGraph G.V

The simple graph underlying a chip-firing multigraph.

Equations

• Utilities.underlyingSimpleGraph G = { Adj := fun (v w : G.V) => numEdges G v w > 0, symm := ⋯, loopless := ⋯ }

@[simp]

theorem Utilities.underlyingSimpleGraph_adj (G : CFGraph) (v w : G.V) : (underlyingSimpleGraph G).Adj v w ↔ numEdges G v w > 0

@[instance_reducible]

instance Utilities.underlyingSimpleGraphDecidableAdj (G : CFGraph) : DecidableRel (underlyingSimpleGraph G).Adj

Equations

• Utilities.underlyingSimpleGraphDecidableAdj G v w = { decide := (Nat.succ 0).ble (numEdges G v w), reflects_decide := ⋯ }

theorem Utilities.graph_connected_iff_underlyingSimpleGraph_connected (G : CFGraph) : graphConnected G ↔ (underlyingSimpleGraph G).Connected

The cut definition of connectivity used by CFGraph agrees with connectivity of the underlying simple graph.