lintegral_iUnion_le — Mathlib

English

Let (s_i) be a countable family of subsets of α and f: α → ℝ≥0∞. Then the lintegral of f over the union ⋃ i s_i is at most the sum of the lintegrals over each s_i.

Русский

Пусть (s_i) задаёт счетную семейство подмножества пространства α, и f: α → ℝ≥0∞. Тогда линегральный интеграл по объединению ⋃_i s_i не превосходит сумму линегралов по каждому s_i.

LaTeX

$$$$\\int_{a \\in \\bigcup_{i} s_i} f(a) \\, d\\mu \\;\\le\\; \\sum_{i} \\int_{a \\in s_i} f(a) \\, d\\mu.$$$$

Lean4

theorem lintegral_iUnion_le [Countable β] (s : β → Set α) (f : α → ℝ≥0∞) :
    ∫⁻ a in ⋃ i, s i, f a ∂μ ≤ ∑' i, ∫⁻ a in s i, f a ∂μ :=
  by
  rw [← lintegral_sum_measure]
  exact lintegral_mono' restrict_iUnion_le le_rfl

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