Theorems · Definition · combinatorics

SimpleGraph.Iso.sumAssoc

{U : Type u_1} →
  {V : Type u_3} →
    {W : Type u_5} → {G : SimpleGraph V} → {H : SimpleGraph W} → {I : SimpleGraph U} → G ⊕g H ⊕g I ≃g G ⊕g (H ⊕g I)

The disjoint sum is associative up to isomorphism. Iso.sumAssoc as a graph isomorphism.

Defined in

Mathlib.Combinatorics.SimpleGraph.Sum

Cited by

5 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Quot.sound