lintegral_prod_right — Mathlib

English

If ν is a finite measure, then x ↦ ν (Prod.mk x)^{-1}(s) is measurable for measurable s.

Русский

Если ν — конечная мера, то x ↦ ν(Prod.mk x)^{-1}(s) измеримо для измеримого s.

LaTeX

$$$\\text{Measurable } x \\mapsto ν(Prod.mk x)^{-1}(s)$ for Measurable s.$$

Lean4

/-- The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
  Tonelli's theorem is measurable.
  This version has the argument `f` in curried form. -/
@[fun_prop, measurability]
theorem lintegral_prod_right [SFinite ν] {f : α → β → ℝ≥0∞} (hf : Measurable (uncurry f)) :
    Measurable fun x => ∫⁻ y, f x y ∂ν :=
  hf.lintegral_prod_right'

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