English
Let f : X → Y and s ⊆ X. Then ContinuousWithinAt f s x is equivalent to PTendsto (PFun.res f s) (nhds x) (nhds (f x)).
Русский
Пусть f : X → Y и s ⊆ X. Тогда ContinuousWithinAt f s x эквивалентно PTendsto (PFun.res f s) (nhds x) (nhds (f x)).
LaTeX
$$$\\mathrm{ContinuousWithinAt}\\ f\\ s\\ x \\iff \\mathrm{PTendsto}\\ (\\mathrm{PFun}.\\mathrm{res}\\ f\\ s)\\ (\\mathcal{N}(x))\\ (\\mathcal{N}(f(x)))$$$
Lean4
theorem continuousWithinAt_iff_ptendsto_res (f : X → Y) {x : X} {s : Set X} :
ContinuousWithinAt f s x ↔ PTendsto (PFun.res f s) (𝓝 x) (𝓝 (f x)) :=
tendsto_iff_ptendsto _ _ _ _