tendsto_nhdsSet_nhds — Mathlib

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'

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