English
For a countable index set and pairwise almost-disjoint family of sets with each set null-measurable, restriction to the union distributes over the union with the sum over the index set.
Русский
Для счётного множества индексов и пары попарно AE-раздельных множеств, каждое из которых нулевым образом измеримо, ограничение на объединение равно сумме ограничений по индексам.
LaTeX
$$$(\text{Pairwise} (AEDisjoint\, \mu\, on\, s) ) \land (\forall i, NullMeasurableSet (s i) \mu) \land (MeasurableSet\,t) \implies \mu.restrict (\bigcup_i s_i)\, t = \sum' i, \mu.restrict (s_i)\, t$$$
Lean4
theorem restrict_union_le (s s' : Set α) : μ.restrict (s ∪ s') ≤ μ.restrict s + μ.restrict s' :=
le_iff.2 fun t ht ↦ by simpa [ht, inter_union_distrib_left] using measure_union_le (t ∩ s) (t ∩ s')
