prodCongr — Mathlib

English

If ab: α ≃ᵐ β and cd: γ ≃ᵐ δ, then α × γ ≃ᵐ β × δ.

Русский

Если существуют измеримые эквивалентности ab: α ≃ᵐ β и cd: γ ≃ᵐ δ, тогда α × γ эквивалентно β × δ в смысле измеримых пространств.

LaTeX

$$$ \text{prodCongr }(ab) (cd): \alpha \times \gamma \simeq^ᵐ \beta \times \delta $$$

Lean4

/-- Products of equivalent measurable spaces are equivalent. -/
def prodCongr (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) : α × γ ≃ᵐ β × δ
    where
  toEquiv := .prodCongr ab.toEquiv cd.toEquiv
  measurable_toFun := (ab.measurable_toFun.comp measurable_id.fst).prodMk (cd.measurable_toFun.comp measurable_id.snd)
  measurable_invFun :=
    (ab.measurable_invFun.comp measurable_id.fst).prodMk (cd.measurable_invFun.comp measurable_id.snd)

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