English
If there exists a limit y of f along nhdsWithin x A, then f tends to extendFrom A f x along nhdsWithin x A.
Русский
Если существует предел y у f при стремлении x к A внутри nhdsWithin, то f стремится к extendFrom A f x в nhdsWithin x.
LaTeX
$$$$ \\text{If } \\exists y, \\mathrm{Tendsto}\\ f\\ (\\mathcal{N}_A x) (\\mathcal{N} y), \\text{ then } \\mathrm{Tendsto}\\ f\\ (\\mathcal{N}_A x) (\\mathcal{N}(\\mathrm{extendFrom}(A,f)(x))). $$$$
Lean4
/-- If `f` converges to some `y` as `x` tends to `x₀` within `A`,
then `f` tends to `extendFrom A f x` as `x` tends to `x₀`. -/
theorem tendsto_extendFrom {A : Set X} {f : X → Y} {x : X} (h : ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)) :
Tendsto f (𝓝[A] x) (𝓝 <| extendFrom A f x) :=
tendsto_nhds_limUnder h
