compProd_assoc' — Mathlib

English

The associativity holder with product rearrangement: (μ ⊗ₘ κ ⊗ₘ η) = (μ ⊗ₘ (κ ⊗ₖ η)) under prodAssoc.

Русский

Существование ассоциативности после перестановки произведения: (μ ⊗ₘ κ ⊗ₘ η) = μ ⊗ₘ (κ ⊗ₖ η) через prodAssoc.

LaTeX

$$$(\\mu \\otimes_{\\mathrm{m}} \\kappa \\otimes_{\\mathrm{m}} \\eta) = (\\mu \\otimes_{\\mathrm{m}} (\\kappa \\otimes_{\\mathrm{k}} \\eta))$ under the appropriate isomorphism MeasurableEquiv.prodAssoc$$

Lean4

/-- `Measure.compProd` is associative. We have to insert `MeasurableEquiv.prodAssoc`
because the products of types `α × β × γ` and `(α × β) × γ` are different. -/
@[simp]
theorem compProd_assoc' {γ : Type*} {mγ : MeasurableSpace γ} {η : Kernel (α × β) γ} :
    (μ ⊗ₘ κ ⊗ₘ η).map MeasurableEquiv.prodAssoc = μ ⊗ₘ (κ ⊗ₖ η) := by simp [← Measure.compProd_assoc]

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