English
If φ is an ae-cover and f is AEStronglyMeasurable on each μ.restrict φ(i), then f is AEStronglyMeasurable with respect to μ.
Русский
Если φ образует ae-покрытие и для каждого i функция f является AEStronglyMeasurable на μ.restrict φ(i), то f является AEStronglyMeasurable и по отношению к μ.
LaTeX
$$$\\forall h\\phi : MeasureTheory.AECover μ l φ,\\ (\\forall i, AEStronglyMeasurable f (μ.restrict (φ i))) \\Rightarrow AEStronglyMeasurable f μ$$$
Lean4
theorem aestronglyMeasurable {β : Type*} [TopologicalSpace β] [PseudoMetrizableSpace β] [l.IsCountablyGenerated]
[l.NeBot] {f : α → β} {φ : ι → Set α} (hφ : AECover μ l φ) (hfm : ∀ i, AEStronglyMeasurable f (μ.restrict <| φ i)) :
AEStronglyMeasurable f μ := by
obtain ⟨u, hu⟩ := l.exists_seq_tendsto
have := aestronglyMeasurable_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
