no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F✝ : ι → α → β
f✝ : α → β
s✝ s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g : ι → α
F : ι → α → β
f : α → β
p : Filter ι
s : Set α
⊢ TendstoUniformlyOn F f p s ↔ Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ 𝓟 s) (𝓤 β)
simp [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]