hasSum_of_disjoint_iUnion — Mathlib

English

For a countable index set β, if the f_i are measurable and pairwise disjoint, then ∑ v(f_i) = v(⋃ f_i).

Русский

Для счётной индексной совокупности β, если множества f_i измеримы и попарно непересекаются, то сумма v(f_i) расходится к v(⋃ f_i).

LaTeX

$$HasSum (fun i => v (f i)) (v (Set.iUnion fun i => f i))$$

Lean4

theorem hasSum_of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwise (Disjoint on f)) :
    HasSum (fun i => v (f i)) (v (⋃ i, f i)) :=
  by
  rcases Countable.exists_injective_nat β with ⟨e, he⟩
  rw [← hasSum_extend_zero he]
  convert m_iUnion v (f := Function.extend e f fun _ ↦ ∅) _ _
  · simp only [Pi.zero_def, Function.apply_extend v, Function.comp_def, empty]
  · exact (iSup_extend_bot he _).symm
  · simp [Function.apply_extend MeasurableSet, Function.comp_def, hm]
  · exact hd.disjoint_extend_bot (he.factorsThrough _)

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