measure_iUnion_le — Mathlib

English

For a countable index set I and sets s i, μ(⋃ i, s i) ≤ ∑' i μ(s i).

Русский

Для счетного множителя индексов I и множеств s_i, μ(⋃ i, s_i) ≤ ∑' i μ(s_i).

LaTeX

$$$\forall I, (I\text{ countable})\; (s:\, I \to Set\ alpha),\; μ(\bigcup_{i} s i) \le \sum' i, μ(s i)$$$

Lean4

theorem measure_iUnion_le [Countable ι] (s : ι → Set α) : μ (⋃ i, s i) ≤ ∑' i, μ (s i) :=
  by
  refine rel_iSup_tsum μ measure_empty (· ≤ ·) (fun t ↦ ?_) _
  calc
    μ (⋃ i, t i) = μ (⋃ i, disjointed t i) := by rw [iUnion_disjointed]
    _ ≤ ∑' i, μ (disjointed t i) := (OuterMeasureClass.measure_iUnion_nat_le _ _ (disjoint_disjointed _))
    _ ≤ ∑' i, μ (t i) := by gcongr; exact disjointed_subset ..

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