setIntegral_compl — Mathlib

English

The integral over the complement equals the full integral minus the integral over the set.

Русский

Интеграл по дополнению равен полному интегралу минус интеграл по множеству.

LaTeX

$$$\\int_{x \\in s^c} f(x) \\,d\\mu = \\int_{x} f(x) \\,d\\mu - \\int_{x \\in s} f(x) \\,d\\mu$$$

Lean4

theorem setIntegral_compl (hs : MeasurableSet s) (hfi : Integrable f μ) :
    ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ - ∫ x in s, f x ∂μ := by
  rw [← integral_add_compl (μ := μ) hs hfi, add_sub_cancel_left]

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