integral_add_compl₀ — Mathlib

English

For null-measurable s, the full integral equals the sum of integrals over s and its complement.

Русский

Для нулевой измеримости s полный интеграл равен сумме интегралов по s и его дополнению.

LaTeX

$$$\\int f \\,d\\mu = \\int_{x \\in s} f(x) \\,d\\mu + \\int_{x \\notin s} f(x) \\,d\\mu$$$

Lean4

theorem integral_add_compl₀ (hs : NullMeasurableSet s μ) (hfi : Integrable f μ) :
    ∫ x in s, f x ∂μ + ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ := by
  rw [← integral_union_ae disjoint_compl_right.aedisjoint hs.compl hfi.integrableOn hfi.integrableOn, union_compl_self,
    setIntegral_univ]

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