English
If a function f is continuous and equals a constant b on s, then f tends to b when restricted to the set s in the nhds sense.
Русский
Если f непрерывна и на s имеет постоянное значение b, то при ограничении до s отображение стремится к b в смысле окрестностей.
LaTeX
$$$\\operatorname{Tendsto}\\ f\\ (\\mathcal{N}^{\\mathrm{set}}(s))\\ (\\mathcal{N}(b))$$$
Lean4
theorem tendsto_nhdsSet_nhds {b : β} {f : α → β} (h : Continuous f) (h' : EqOn f (fun _ ↦ b) s) :
Tendsto f (𝓝ˢ s) (𝓝 b) := by
rw [← nhdsSet_singleton]
exact h.tendsto_nhdsSet h'