English
If φ is an ae-cover and f is a function whose restriction to each φ(i) is almost everywhere measurable, then f is almost everywhere measurable with respect to μ.
Русский
Если φ образует ae-покрытие и f таково, что ограничение f на каждый φ(i) измеримо почти везде, то f измеримо относительно μ почти повсюду.
LaTeX
$$$\\forall h\\phi : MeasureTheory.AECover μ l φ, \\ (\\forall i, AEMeasurable f (μ.restrict (φ i))) \\Rightarrow AEMeasurable f μ$$$
Lean4
theorem aemeasurable {β : Type*} [MeasurableSpace β] [l.IsCountablyGenerated] [l.NeBot] {f : α → β} {φ : ι → Set α}
(hφ : AECover μ l φ) (hfm : ∀ i, AEMeasurable f (μ.restrict <| φ i)) : AEMeasurable f μ :=
by
obtain ⟨u, hu⟩ := l.exists_seq_tendsto
have := aemeasurable_iUnion_iff.mpr fun n : ℕ => hfm (u n)
rwa [Measure.restrict_eq_self_of_ae_mem] at this
filter_upwards [hφ.ae_eventually_mem] with x hx using mem_iUnion.mpr (hu.eventually hx).exists
