case intro
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n)
h_tendsto : TendstoInMeasure μ f u g
ns : ℕ → ι
hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
⊢ AEMeasurable g
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n)
h_tendsto : TendstoInMeasure μ f u g
⊢ AEMeasurable g
obtain ⟨ns, hns⟩ := h_tendsto.exists_seq_tendsto_ae'
no goals
case intro
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n)
h_tendsto : TendstoInMeasure μ f u g
ns : ℕ → ι
hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
⊢ AEMeasurable g
exact aemeasurable_of_tendsto_metrizable_ae atTop (fun n => hf (ns n)) hns