lintegral_prod_left — Mathlib

English

The Lebesgue integral is measurable, dual version with left-right symmetry.

Русский

Лебегов интеграл измерим; симметричная версия слева направо.

LaTeX

$$$\\text{Measurable } f \\Rightarrow \\text{Measurable}(y \\mapsto \\int f(x,y) dν(x))$$$

Lean4

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

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