sumComm — Mathlib

English

The disjoint sum is commutative up to isomorphism; there exists a graph isomorphism between G ⊕g H and H ⊕g G.

Русский

Дизъюнктивное сложение графов коммутативно по отношению к изоморфизму; существует графовый изоморфизм между G ⊕g H и H ⊕g G.

LaTeX

$$$(G \oplus_g H) \cong_g (H \oplus_g G).$$$

Lean4

/-- The disjoint sum is commutative up to isomorphism. `Iso.sumComm` as a graph isomorphism. -/
@[simps!]
def sumComm : G ⊕g H ≃g H ⊕g G :=
  ⟨Equiv.sumComm α β, by rintro (u | u) (v | v) <;> simp⟩

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