lintegral_inter_add_diff — Mathlib

English

For any sets A and B and a function f ≥ 0, the lintegral over A equals the sum of the lintegrals over A ∩ B and A \\ B.

Русский

Для любых множеств A и B и функции f ≥ 0 линегральный интеграл по A равен сумме линегралов по A ∩ B и A \\ B.

LaTeX

$$$$\\int_{a\\in A} f(a) \\, d\\mu = \\int_{a\\in A \\cap B} f(a) \\, d\\mu + \\int_{a\\in A \\setminus B} f(a) \\, d\\mu.$$$$

Lean4

theorem lintegral_inter_add_diff {B : Set α} (f : α → ℝ≥0∞) (A : Set α) (hB : MeasurableSet B) :
    ∫⁻ x in A ∩ B, f x ∂μ + ∫⁻ x in A \ B, f x ∂μ = ∫⁻ x in A, f x ∂μ := by
  rw [← lintegral_add_measure, restrict_inter_add_diff _ hB]

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