apply_iUnion_le — Mathlib

English

If μ is a finite measure and f(n) is a sequence of sets with Summable μ(f(n)), then μ(⋃_n f(n)) ≤ ∑' μ(f(n)).

Русский

Если μ — конечная мера и f(n) — последовательность множеств с суммируемыми μ(f(n)), то μ(⋃_n f(n)) ≤ ∑' μ(f(n)).

LaTeX

$$$\text{Summable}(\lambda n. μ(f(n))) \Rightarrow μ\left(\bigcup_{n} f(n)\right) \le \sum_{n}^{\infty} μ(f(n))$$$

Lean4

theorem apply_iUnion_le {μ : FiniteMeasure Ω} {f : ℕ → Set Ω} (hf : Summable fun n ↦ μ (f n)) :
    μ (⋃ n, f n) ≤ ∑' n, μ (f n) := by
  simpa [← ENNReal.coe_le_coe, ENNReal.coe_tsum hf] using MeasureTheory.measure_iUnion_le f

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