sumAssoc — Mathlib

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⟩

Похожие утверждения