addContent_sUnion — Mathlib

English

Value on union of a finite collection is the sum over the pieces (under suitable disjointness/subset conditions).

Русский

Значение на объединении конечной коллекции равно сумме по частям (при подходящих условиях раздельности).

LaTeX

$$m(⋃ i ∈ I, S_i) = ∑ i ∈ I, m(S_i)$$

Lean4

theorem addContent_sUnion (h_ss : ↑I ⊆ C) (h_dis : PairwiseDisjoint (I : Set (Set α)) id) (h_mem : ⋃₀ ↑I ∈ C) :
    m (⋃₀ I) = ∑ u ∈ I, m u :=
  m.sUnion' I h_ss h_dis h_mem

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