prodComm — Mathlib

English

Products of measurable spaces are symmetric; α × β ≃ᵐ β × α.

Русский

Произведения пространств меры симметричны: α × β ≃ᵐ β × α.

LaTeX

$$$ \text{prodComm}: \alpha \times \beta \simeq^ᵐ \beta \times \alpha $$$

Lean4

/-- Products of measurable spaces are symmetric. -/
def prodComm : α × β ≃ᵐ β × α where
  toEquiv := .prodComm α β
  measurable_toFun := measurable_id.snd.prodMk measurable_id.fst
  measurable_invFun := measurable_id.snd.prodMk measurable_id.fst

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