α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (l ×ˢ 𝓟 s) (𝓤 β)
u : ℕ → ι
hu : Tendsto u atTop l
⊢ Tendsto (fun q => (f q.snd, F (u q.fst) q.snd)) (atTop ×ˢ 𝓟 s) (𝓤 β)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
h : TendstoUniformlyOn F f l s
u : ℕ → ι
hu : Tendsto u atTop l
⊢ TendstoUniformlyOn (fun n => F (u n)) f atTop s
rw [tendstoUniformlyOn_iff_tendsto] at h⊢
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (l ×ˢ 𝓟 s) (𝓤 β)
u : ℕ → ι
hu : Tendsto u atTop l
⊢ Tendsto (fun q => (f q.snd, F (u q.fst) q.snd)) (atTop ×ˢ 𝓟 s) (𝓤 β)
exact h.comp ((hu.comp tendsto_fst).prod_mk tendsto_snd)