sumCongr — Mathlib

English

Sums of measurable spaces are symmetric: if ab: α ≃ᵐ β and cd: γ ≃ᵐ δ, then α ⊕ γ ≃ᵐ β ⊕ δ.

Русский

Суммы пространств меры симметричны: если ab: α ≃ᵐ β и cd: γ ≃ᵐ δ, то α ⊕ γ ≃ᵐ β ⊕ δ.

LaTeX

$$$ \text{sumCongr }(ab) (cd): α \oplus γ \simeq^ᵐ β \oplus δ $$$

Lean4

/-- Sums of measurable spaces are symmetric. -/
def sumCongr (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) : α ⊕ γ ≃ᵐ β ⊕ δ
    where
  toEquiv := .sumCongr ab.toEquiv cd.toEquiv
  measurable_toFun := ab.measurable.sumMap cd.measurable
  measurable_invFun := ab.symm.measurable.sumMap cd.symm.measurable

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