English
If a dense set A gives limits for every x, then extendFrom A f is globally continuous.
Русский
Если плотная подмножество A задаёт пределы для каждого x, то extendFrom A f непрерывна по всей области.
LaTeX
$$$$ \\text{If } \\text{Dense}(A) \\text{ and } \\forall x, \\exists y, \\mathrm{Tendsto}\\ f (\\mathcal{N}_A x) (\\mathcal{N} y) \\Rightarrow \\mathrm{Continuous}(\\mathrm{extendFrom}(A,f)). $$$$
Lean4
/-- If a function `f` to a T₃ space `Y` has a limit within a
dense set `A` for any `x`, then `extendFrom A f` is continuous. -/
theorem continuous_extendFrom [RegularSpace Y] {f : X → Y} {A : Set X} (hA : Dense A)
(hf : ∀ x, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)) : Continuous (extendFrom A f) :=
by
rw [← continuousOn_univ]
exact continuousOn_extendFrom (fun x _ ↦ hA x) (by simpa using hf)
