extendFrom_eq — Mathlib

English

If x belongs to the closure of A and f tends to y along nhdsWithin x A, then extendFrom A f x = y.

Русский

Если x принадлежит замыканию A и f сходится к y вдоль nhdsWithin x A, тогда extendFrom A f x = y.

LaTeX

$$$$ x \\in \\overline{A} \\land \\mathrm{Tendsto}\\ f\\ (\\mathcal{N}_A x) (\\mathcal{N} y) \\Rightarrow \\mathrm{extendFrom}(A,f)(x) = y. $$$$

Lean4

theorem extendFrom_eq [T2Space Y] {A : Set X} {f : X → Y} {x : X} {y : Y} (hx : x ∈ closure A)
    (hf : Tendsto f (𝓝[A] x) (𝓝 y)) : extendFrom A f x = y :=
  haveI := mem_closure_iff_nhdsWithin_neBot.mp hx
  tendsto_nhds_unique (tendsto_nhds_limUnder ⟨y, hf⟩) hf

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