lintegral_union — Mathlib

English

If B is measurable and A and B are disjoint, then the lintegral over A ∪ B equals the sum of the lintegrals over A and over B.

Русский

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

LaTeX

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

Lean4

theorem lintegral_union {f : α → ℝ≥0∞} {A B : Set α} (hB : MeasurableSet B) (hAB : Disjoint A B) :
    ∫⁻ a in A ∪ B, f a ∂μ = ∫⁻ a in A, f a ∂μ + ∫⁻ a in B, f a ∂μ := by
  rw [restrict_union hAB hB, lintegral_add_measure]

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