English
The disjoint sum is associative up to isomorphism: (G ⊕g H) ⊕g I ≃g G ⊕g (H ⊕g I).
Русский
Дизъюнктивное сложение графов ассоциативно по отношению к изоморфизму: (G ⊕g H) ⊕g I ≃g G ⊕g (H ⊕g I).
LaTeX
$$$((G \oplus_g H) \oplus_g I) \cong_g (G \oplus_g (H \oplus_g I)).$$$
Lean4
/-- The disjoint sum is associative up to isomorphism. `Iso.sumAssoc` as a graph isomorphism. -/
@[simps!]
def sumAssoc {I : SimpleGraph γ} : (G ⊕g H) ⊕g I ≃g G ⊕g (H ⊕g I) :=
⟨Equiv.sumAssoc α β γ, by rintro ((u | u) | u) ((v | v) | v) <;> simp⟩