no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.197144
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α)
rw [ContinuousAt, tendsto_nhds_right]