English
Let (s_i)_{i∈ι} be a family of sets. If f is AEMeasurable with respect to μ restricted to each s_i, then f is AEMeasurable with respect to μ restricted to the union ⋃_i s_i.
Русский
Пусть (s_i) — счетная семейство подмножеств. Если функция f является АЕ-измеримой относительно меры μ, ограниченной на каждое s_i, то она является АЕ-измеримой относительно меры μ, ограниченной объединением ⋃_i s_i.
LaTeX
$$$\left(\forall i, \mathrm{AEMeasurable}(f, \mu\restriction s_i)\right) \rightarrow \mathrm{AEMeasurable}(f, \mu\restriction (\bigcup_i s_i))$$$
Lean4
@[measurability]
protected theorem iUnion [Countable ι] {s : ι → Set α} (h : ∀ i, AEMeasurable f (μ.restrict (s i))) :
AEMeasurable f (μ.restrict (⋃ i, s i)) :=
(sum_measure h).mono_measure <| restrict_iUnion_le
