toMeasure_prod — Mathlib

English

For any measurable set s ⊆ α × β, (μ.prod ν)(s) equals the NNReal of the integral ∫⁻ x ν.toMeasure (Prod.mk x⁻¹' s) dμ.

Русский

Для любого измеримого множества s ⊆ α × β значение (μ.prod ν)(s) равно toNNReal от интеграла ∫⁻ x ν.toMeasure (Prod.mk x⁻¹' s) dμ.

LaTeX

$$$ (\mu \mathrm{prod} \nu)(s) = \operatorname{toNNReal}\left(\int^{-} x\, \nu.toMeasure (\mathrm{Prod.mk}\ x^{-1} s) \partial \mu\right)$$$

Lean4

@[simp]
theorem toMeasure_prod : (μ.prod ν).toMeasure = μ.toMeasure.prod ν.toMeasure :=
  rfl

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