case intro
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
f✝ : ℕ → α → E
g✝ : α → E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ns : ℕ → ι
h_tendsto_ns : Tendsto ns atTop u
⊢ ∃ ns, TendstoInMeasure μ (fun n => f (ns n)) atTop g
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
f✝ : ℕ → α → E
g✝ : α → E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
⊢ ∃ ns, TendstoInMeasure μ (fun n => f (ns n)) atTop g
obtain ⟨ns, h_tendsto_ns⟩ : ∃ ns : ℕ → ι, Tendsto ns atTop u := exists_seq_tendsto u
no goals
case intro
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
f✝ : ℕ → α → E
g✝ : α → E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ns : ℕ → ι
h_tendsto_ns : Tendsto ns atTop u
⊢ ∃ ns, TendstoInMeasure μ (fun n => f (ns n)) atTop g
exact ⟨ns, fun ε hε => (hfg ε hε).comp h_tendsto_ns⟩