α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ p') (𝓤 β)
g : γ → α
⊢ Tendsto (fun q => ((f ∘ g) q.snd, (F q.fst ∘ g) q.snd)) (p ×ˢ comap g p') (𝓤 β)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : TendstoUniformlyOnFilter F f p p'
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (comap g p')
rw [tendstoUniformlyOnFilter_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✝ : ι → α
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ p') (𝓤 β)
g : γ → α
⊢ Tendsto (fun q => ((f ∘ g) q.snd, (F q.fst ∘ g) q.snd)) (p ×ˢ comap g p') (𝓤 β)
exact h.comp (tendsto_id.prod_map tendsto_comap)