lintegral_kernel — Mathlib

English

If f is measurable (uncurry f), then for any measurable set s ⊆ β, the map a ↦ ∫⁻ b in s, f(a,b) dκ a is measurable.

Русский

Если f измеримо (uncurry f), то для любого измеримого s ⊆ β отображение a ↦ ∫⁻ b в s f(a,b) dκ a измеримо.

LaTeX

$$$\\text{Measurable}\\left( a \\mapsto \\int⁻ b \\in s\\, f(a,b) \\, ∂κ a \\right)$$$

Lean4

@[fun_prop]
theorem _root_.Measurable.lintegral_kernel {κ : Kernel α β} {f : β → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun a => ∫⁻ b, f b ∂κ a := by fun_prop

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