lintegral_indicator_const₀ — Mathlib

English

For any measurable f and any constant c, the lintegral of s.indicator (constant c) equals c times the measure over s.

Русский

Для любой измеримой f и константы c линеграл s.indicator c равен c умножить на μ(s).

LaTeX

$$$$ \\int^- a, s.indicator (c) a \\, d\\mu = c \\cdot \\mu(s). $$$$

Lean4

theorem lintegral_indicator_const₀ {s : Set α} (hs : NullMeasurableSet s μ) (c : ℝ≥0∞) :
    ∫⁻ a, s.indicator (fun _ => c) a ∂μ = c * μ s := by rw [lintegral_indicator₀ hs, setLIntegral_const]

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