English
If i ranges over a countable index set and each f is AEMeasurable with respect to μ(i), then f is AEMeasurable with respect to the sum of the μ(i).
Русский
Если индексный набор счётен и каждая функция f является AЕ-измеримой относительно μ(i), то f является AЕ-измеримой относительно суммы μ(i).
LaTeX
$$$[Countable]\\ ι \\\\rightarrow \\\\Measure α \\\\quad (\\\\forall i, \\\\text{AEMeasurable}(f,\\\\mu i)) \\\\Rightarrow \\\\text{AEMeasurable}(f,\\\\sum μ)$$$
Lean4
theorem ae_inf_principal_eq_mk {s} (h : AEMeasurable f (μ.restrict s)) : f =ᶠ[ae μ ⊓ 𝓟 s] h.mk f :=
le_ae_restrict h.ae_eq_mk