boxProdAssoc — Mathlib

English

Box product is associative up to isomorphism: (G □ H) □ I ≃g G □ (H □ I).

Русский

BoxProd ассоциативен до изоморфизма: (G □ H) □ I ≃g G □ (H □ I).

LaTeX

$$$G \\Box H \\Box I \\cong_g G \\Box (H \\Box I)$$$

Lean4

/-- The box product is associative up to isomorphism. `Equiv.prodAssoc` as a graph isomorphism. -/
@[simps!]
def boxProdAssoc (I : SimpleGraph γ) : G □ H □ I ≃g G □ (H □ I) :=
  ⟨Equiv.prodAssoc _ _ _, fun {x y} => by
    simp only [boxProd_adj, Equiv.prodAssoc_apply, or_and_right, or_assoc, Prod.ext_iff, and_assoc,
      @and_comm (x.fst.fst = _)]⟩

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