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