prodComm — Mathlib

English

The triple product space (X × Y) × Z is homeomorphic to X × (Y × Z).

Русский

Тройное произведение (X × Y) × Z гомеоморфно пространству X × (Y × Z).

LaTeX

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

Lean4

/-- `X × Y` is homeomorphic to `Y × X`. -/
def prodComm : X × Y ≃ₜ Y × X
    where
  continuous_toFun := continuous_snd.prodMk continuous_fst
  continuous_invFun := continuous_snd.prodMk continuous_fst
  toEquiv := Equiv.prodComm X Y

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