Edge colourings of a SimpleGraph

SimpleGraph.IsEdgeColouring H c asserts that c : ι → SimpleGraph V is a partition of the edges of H into colour classes indexed by ι. The classes must (1) cover H (H = ⨆ i, c i) and (2) be pairwise disjoint (each edge belongs to exactly one class).

This unifies the previous local IsNEdgeColouring (ι = Fin n) and IsCountableEdgeColouring (ι = ℕ) shapes used in FormalConjectures/ErdosProblems/596.lean. The two are now special cases of IsEdgeColouring parameterised by the index type.

def SimpleGraph.IsEdgeColouring {V : Type u_1} {ι : Type u_2} (H : SimpleGraph V) (c : ι → SimpleGraph V) : Prop

IsEdgeColouring H c asserts that c : ι → SimpleGraph V is a partition of the edges of H: the colour classes cover H (H = ⨆ i, c i) and are pairwise disjoint.

Equations

• H.IsEdgeColouring c = (H = ⨆ (i : ι), c i ∧ ∀ (i j : ι), i ≠ j → Disjoint (c i) (c j))