setLIntegral_compl — Mathlib

English

If s is measurable and the integral of f over s is finite, then the integral over complement s^c equals the total minus the part over s.

Русский

Если s измеримо и интеграл по s конечен, то интеграл по дополнению s равен общему интегралу минус интеграл по s.

LaTeX

$$$$\\int_{a \\in s^{\\complement}} f(a) \\, d\\mu = \\int_{a} f(a) \\, d\\mu - \\int_{a \\in s} f(a) \\, d\\mu.$$$$

Lean4

theorem setLIntegral_compl {f : α → ℝ≥0∞} {s : Set α} (hsm : MeasurableSet s) (hfs : ∫⁻ x in s, f x ∂μ ≠ ∞) :
    ∫⁻ x in sᶜ, f x ∂μ = ∫⁻ x, f x ∂μ - ∫⁻ x in s, f x ∂μ := by
  rw [← lintegral_add_compl (μ := μ) f hsm, ENNReal.add_sub_cancel_left hfs]

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