prodAssoc — Mathlib

English

Products of measurable spaces are associative up to a measurable equivalence: (α × β) × γ ≃ᵐ α × (β × γ).

Русский

Произведения пространств меры ассоциативны в смысле измеримых эквивалентностей: (α × β) × γ ≃ᵐ α × (β × γ).

LaTeX

$$$ \text{prodAssoc}: (\alpha \times \beta) \times \gamma \simeq^ᵐ \alpha \times (\beta \times \gamma) $$$

Lean4

/-- Products of measurable spaces are associative. -/
def prodAssoc : (α × β) × γ ≃ᵐ α × β × γ where
  toEquiv := .prodAssoc α β γ
  measurable_toFun := measurable_fst.fst.prodMk <| measurable_fst.snd.prodMk measurable_snd
  measurable_invFun := (measurable_fst.prodMk measurable_snd.fst).prodMk measurable_snd.snd

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