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 = _)]⟩