English
If x belongs to the closure of A and f has a limit y along nhdsWithin x A, then extendFrom A f x equals y.
Русский
Если x лежит в замыкании A и у f есть предел y при сходящемся к x внутри A, то extendFrom A f x = y.
LaTeX
$$$$ x \\in \\overline{A} \\quad\\land\\quad \\mathrm{Tendsto}\\ f\\ (\\mathcal{N}_A x)\\ (\\mathcal{N} y) \\;\textrm{implies}\; \\mathrm{extendFrom}(A,f)(x) = y. $$$$
Lean4
/-- Extend a function from a set `A`. The resulting function `g` is such that
at any `x₀`, if `f` converges to some `y` as `x` tends to `x₀` within `A`,
then `g x₀` is defined to be one of these `y`. Else, `g x₀` could be anything. -/
def extendFrom (A : Set X) (f : X → Y) : X → Y := fun x ↦ @limUnder _ _ _ ⟨f x⟩ (𝓝[A] x) f
