prod_apply_symm — Mathlib

English

For measurable s ⊆ α and t ⊆ β, (μ.prod ν)(s ×ˢ t) = μ s · ν t.

Русский

Для измеримых s ⊆ α и t ⊆ β выполняется (μ.prod ν)(s ×ˢ t) = μ(s) ν(t).

LaTeX

$$$ (\mu \mathrm{prod} \nu)(s \times^{\mathrm{ˢ}} t) = \mu(s) \cdot \nu(t) $$$

Lean4

theorem prod_apply_symm (s : Set (α × β)) (s_mble : MeasurableSet s) :
    μ.prod ν s = ENNReal.toNNReal (∫⁻ y, μ.toMeasure ((fun x ↦ ⟨x, y⟩) ⁻¹' s) ∂ν) := by
  simp [coeFn_def, Measure.prod_apply_symm s_mble]

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