lintegral_indicator_const — Mathlib

English

If the support of f is contained in s, then the integral over s equals the unrestricted integral.

Русский

Если опора функции f ⊆ s, то интеграл по s равен интегралу по всей области.

LaTeX

$$$$ f.\\operatorname{support} \\subseteq s \\Rightarrow \\int^-_{x \\in s} f(x) \\, d\\mu = \\int^-_{x} f(x) \\, d\\mu. $$$$

Lean4

theorem lintegral_indicator_const {s : Set α} (hs : MeasurableSet s) (c : ℝ≥0∞) :
    ∫⁻ a, s.indicator (fun _ => c) a ∂μ = c * μ s :=
  lintegral_indicator_const₀ hs.nullMeasurableSet c

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