Cardinal edge accounting for arbitrary matching decompositions

The edge equivalence gives an indexed cardinal sum without finiteness of the vertices, edges, or palette. The lift only reconciles the two type universes. This is distinct from natural-number counting, which requires finite edges.

theorem SimpleGraph.MatchingDecomposition.cardinal_edges_eq_sum {V : Type u} {C : Type v} {G : SimpleGraph V} (D : G.MatchingDecomposition C) : Cardinal.lift.{v, u} (Cardinal.mk ↑G.edgeSet) = Cardinal.sum fun (c : C) => Cardinal.mk ↑(D.matching c).edgeSet

The cardinality of the graph edges is the indexed cardinal sum of its matching classes. No finiteness assumptions are required, and unused colours contribute zero.