integral_add_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) \\mathrm{d}\\mu = \\int f \\,d\\mu - \\int_{x \\in s} f(x) \\,d\\mu$$$

Lean4

theorem integral_add_compl (hs : MeasurableSet s) (hfi : Integrable f μ) :
    ∫ x in s, f x ∂μ + ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ :=
  integral_add_compl₀ hs.nullMeasurableSet hfi

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