m_iUnion — Mathlib

English

Let v be a vector measure on α with values in M. If (f_i) is a sequence of pairwise disjoint measurable subsets of α, then the series ∑_i v(f_i) converges to v(⋃_i f_i).

Русский

Пусть v — векторная мера на α с значениям в M. Если (f_i) — последовательность попарно непересекающихся измеримых подмножеств α, то сумма по i от v(f_i) сходится к v(⋃_i f_i).

LaTeX

$$$HasSum (\\lambda i: v (f i)) (v (\\bigcup_i f_i))$$$

Lean4

theorem m_iUnion (v : VectorMeasure α M) {f : ℕ → Set α} (hf₁ : ∀ i, MeasurableSet (f i))
    (hf₂ : Pairwise (Disjoint on f)) : HasSum (fun i => v (f i)) (v (⋃ i, f i)) :=
  v.m_iUnion' hf₁ hf₂

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