prod_apply — Mathlib

English

The product measure of a rectangle s × t equals the product of the individual measures: μ × ν (s ×ˢ t) = μ(s) · ν(t).

Русский

Произведение меры на прямоугольнике s × t равно произведению мер: μ × ν (s × t) = μ(s) · ν(t).

LaTeX

$$$\mu \mathrm{.prod} ν (s \timesˢ t) = μ(s) \cdot ν(t)$$$

Lean4

theorem prod_apply {s : Set (α × β)} (hs : MeasurableSet s) : μ.prod ν s = ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ := by
  simp_rw [Measure.prod, bind_apply hs (Measurable.map_prodMk_left (ν := ν)).aemeasurable,
    map_apply measurable_prodMk_left hs]

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