α : Type u
β : Type v
X : Type ?u.289039
ι : Type ?u.289042
inst✝ : PseudoMetricSpace α
f : β → α
x : Filter β
a : α
⊢ Tendsto ((fun x => dist x a) ∘ f) x (𝓝 0) ↔ Tendsto (fun b => dist (f b) a) x (𝓝 0)
α : Type u
β : Type v
X : Type ?u.289039
ι : Type ?u.289042
inst✝ : PseudoMetricSpace α
f : β → α
x : Filter β
a : α
⊢ Tendsto f x (𝓝 a) ↔ Tendsto (fun b => dist (f b) a) x (𝓝 0)
rw [← nhds_comap_dist a, tendsto_comap_iff]
no goals
α : Type u
β : Type v
X : Type ?u.289039
ι : Type ?u.289042
inst✝ : PseudoMetricSpace α
f : β → α
x : Filter β
a : α
⊢ Tendsto ((fun x => dist x a) ∘ f) x (𝓝 0) ↔ Tendsto (fun b => dist (f b) a) x (𝓝 0)
rfl