lintegral_add_compl — Mathlib

English

If A is measurable, then the lintegral over A plus the lintegral over its complement equals the lintegral over the whole space.

Русский

Если A измеримо, то линегральный интеграл по A плюс линегральный интеграл по дополнению A равен линегральному интегралу по всему пространству.

LaTeX

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

Lean4

theorem lintegral_add_compl (f : α → ℝ≥0∞) {A : Set α} (hA : MeasurableSet A) :
    ∫⁻ x in A, f x ∂μ + ∫⁻ x in Aᶜ, f x ∂μ = ∫⁻ x, f x ∂μ := by
  rw [← lintegral_add_measure, Measure.restrict_add_restrict_compl hA]

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