tendsto_nhdsSet — Mathlib

English

If f is continuous and MapsTo f s t, then Tendsto f on nhdsSet s to nhdsSet t holds; i.e. continuity transfers to the subspace level.

Русский

Если f непрерывна и отображает s в t, тогда Tendsto f на nhdsSet s в nhdsSet t выполняется; непрерывность переносится на подпроизведение.

LaTeX

$$$\\operatorname{Tendsto}\\ f\\ (\\mathcal{N}(s))\\ (\\mathcal{N}(t))$$$

Lean4

/-- Preimage of a set neighborhood of `t` under a continuous map `f` is a set neighborhood of `s`
provided that `f` maps `s` to `t`. -/
theorem tendsto_nhdsSet {f : α → β} {t : Set β} (hf : Continuous f) (hst : MapsTo f s t) : Tendsto f (𝓝ˢ s) (𝓝ˢ t) :=
  hf.continuousOn.tendsto_nhdsSet univ_mem hst

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