case intro
α : Type u_3
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_1
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
u : ℕ → ι
hu : Tendsto u atTop l
⊢ AEMeasurable f
α : Type u_3
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_1
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
⊢ AEMeasurable f
obtain ⟨u, hu⟩ := l.exists_seq_tendsto
case intro
α : Type u_3
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_1
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f
⊢ AEMeasurable f
case intro
α : Type u_3
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_1
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
u : ℕ → ι
hu : Tendsto u atTop l
⊢ AEMeasurable f
have := aemeasurable_iUnion_iff.mpr fun n : ℕ => hfm (u n)
case intro.hs
α : Type u_3
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_1
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f
⊢ ∀ᵐ (x : α) ∂μ, x ∈ ⋃ (i : ℕ), φ (u i)
case intro
α : Type u_3
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_1
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f
⊢ AEMeasurable f
rwa [Measure.restrict_eq_self_of_ae_mem] at this
no goals
case intro.hs
α : Type u_3
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_1
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f
⊢ ∀ᵐ (x : α) ∂μ, x ∈ ⋃ (i : ℕ), φ (u i)
filter_upwards [hφ.ae_eventually_mem] with x hx using
  mem_iUnion.mpr (hu.eventually hx).exists