α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.196937
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto ((fun y => (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.196937
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)
rw [nhds_eq_comap_uniformity', tendsto_comap_iff]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.196937
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto ((fun y => (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)
rfl