extend_iUnion_le_tsum_nat — Mathlib

English

For measurable m0 and mU, the extension over a Nat-indexed iUnion is bounded by tsum of extensions.

Русский

При m0 и mU расширение над iUnion по Nat ограничено tsum расширений.

LaTeX

$$$\\forall s: \\mathbb{N} \\to Set\\alpha, \\ \\mathrm{Extend\\ iUnion\\le\\ tsum\\_nat}(m, s)$$$

Lean4

theorem extend_iUnion_le_tsum_nat : ∀ s : ℕ → Set α, extend m (⋃ i, s i) ≤ ∑' i, extend m (s i) :=
  by
  refine extend_iUnion_le_tsum_nat' MeasurableSet.iUnion ?_; intro f h
  simp +singlePass only [iUnion_disjointed.symm]
  rw [mU (MeasurableSet.disjointed h) (disjoint_disjointed _)]
  refine ENNReal.tsum_le_tsum fun i => ?_
  rw [← extend_eq m, ← extend_eq m]
  exact extend_mono m0 mU (MeasurableSet.disjointed h _) (disjointed_le f _)

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