iUnion_eq_of_caratheodory — Mathlib

English

If s i are measurable, then the union over i is equal to the sum of measures; m(⋃ i, s i) = ∑' i, m(s i).

Русский

Если множества s_i измеримы, то мера объединения равна сумме мер: m(⋃ i, s i) = ∑' i, m(s_i).

LaTeX

$$m (⋃ i, s i) = ∑' i, m (s i)$$

Lean4

protected theorem iUnion_eq_of_caratheodory {s : ℕ → Set α} (h : ∀ i, MeasurableSet[OuterMeasure.caratheodory m] (s i))
    (hd : Pairwise (Disjoint on s)) : m (⋃ i, s i) = ∑' i, m (s i) :=
  f_iUnion m h hd

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