prodAssoc — Mathlib

English

There is a homeomorphism (X × Y) × W × Z ≃ₜ (X × W) × Y × Z expressing four‑way commutativity of products.

Русский

Существует гомеоморфизм (X × Y) × W × Z ≃ₜ (X × W) × Y × Z, выражающий четырехкратную перестановку произведений.

LaTeX

$$$(X \times Y) \times W \times Z \simeq_t (X \times W) \times Y \times Z$$$

Lean4

/-- `(X × Y) × Z` is homeomorphic to `X × (Y × Z)`. -/
def prodAssoc : (X × Y) × Z ≃ₜ X × Y × Z
    where
  continuous_toFun := continuous_fst.fst.prodMk (continuous_fst.snd.prodMk continuous_snd)
  continuous_invFun := (continuous_fst.prodMk continuous_snd.fst).prodMk continuous_snd.snd
  toEquiv := Equiv.prodAssoc X Y Z

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