setLIntegral_indicator — Mathlib

English

If s is NullMeasurableSet with respect to μ, then the lintegral of s.indicator f equals the lintegral over s of f.

Русский

Если s является NullMeasurableSet относительно μ, то интеграл линеграла от s.indicator f равен интегралу f на s.

LaTeX

$$$$ \\int^- a, s.indicator f(a) \\, d\\mu = \\int^- a \\in s, f(a) \\, d\\mu. $$$$

Lean4

theorem setLIntegral_indicator {s t : Set α} (hs : MeasurableSet s) (f : α → ℝ≥0∞) :
    ∫⁻ a in t, s.indicator f a ∂μ = ∫⁻ a in s ∩ t, f a ∂μ := by
  rw [lintegral_indicator hs, Measure.restrict_restrict hs]

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