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₀ (f : α → ℝ≥0∞) {s t : Set α} (hs : NullMeasurableSet s (μ.restrict t)) :
    ∫⁻ a in t, s.indicator f a ∂μ = ∫⁻ a in s ∩ t, f a ∂μ := by
  rw [lintegral_indicator₀ hs, Measure.restrict_restrict₀ hs]

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