intro s hs
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
⊢ Tendsto (fun x => (f x, ℓ)) p (𝓤 β)
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ s ∈ map (fun x => (f x, ℓ)) p