English
Let (s_i) be a countable family of sets. Then f is AEMeasurable with respect to μ restricted to the union if and only if f is AEMeasurable with respect to μ restricted to each s_i.
Русский
Пусть (s_i) — счетная семейство; тогда f является АЕ-измеримой на μ, ограниченной объединением, тогда и только тогда она является АЕ-измеримой на μ, ограниченной каждому s_i.
LaTeX
$$$\mathrm{AEMeasurable}(f, \mu\restriction (\bigcup_i s_i)) \iff \forall i, \mathrm{AEMeasurable}(f, \mu\restriction s_i)$$$
Lean4
@[simp]
theorem _root_.aemeasurable_iUnion_iff [Countable ι] {s : ι → Set α} :
AEMeasurable f (μ.restrict (⋃ i, s i)) ↔ ∀ i, AEMeasurable f (μ.restrict (s i)) :=
⟨fun h _ => h.mono_measure <| restrict_mono (subset_iUnion _ _) le_rfl, AEMeasurable.iUnion⟩
