continuousWithinAt_iff_ptendsto_res

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 _ _ _ _

Похожие утверждения