A switch of two disjoint edges

Monien and Preis normalize a side by replacing edges a-b and c-d with edges a-c and b-d. The four endpoints are distinct and the new edges must be absent, so this operation preserves each vertex degree.

structure Algebraic.Cutwidth.Bisection.Switchable {W : Type} (H : SimpleGraph W) (a b c d : W) : Prop

The two old edges are disjoint and the two new edges are absent. The old adjacencies also imply a ≠ b and c ≠ d.

• ab : H.Adj a b
• cd : H.Adj c d
• ac : ¬H.Adj a c
• bd : ¬H.Adj b d
• distinct : a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d

def Algebraic.Cutwidth.Bisection.switchEdges {W : Type} (H : SimpleGraph W) (a b c d : W) : SimpleGraph W

Delete a-b and c-d, then add a-c and b-d.

Equations

• Algebraic.Cutwidth.Bisection.switchEdges H a b c d = H.deleteEdges {s(a, b), s(c, d)} ⊔ SimpleGraph.edge a c ⊔ SimpleGraph.edge b d