tendsto_nhdsWithin_image — Mathlib

English

If f is continuous within s at x, then it tends to f x along nhdsWithin x s and toward nhdsWithin (f x) (image f s).

Русский

Если f непрерывна внутри s в точке x, то она стремится к f(x) вдоль nhdsWithin x s и к nhdsWithin (f x) (образ f в s).

LaTeX

$$$ (h : ContinuousWithinAt f s x) : Tendsto f (\\mathcal{N} [s] x) (\\mathcal{N} [(\\text{image } f s)] (f x)) $$$

Lean4

theorem tendsto_nhdsWithin_image (h : ContinuousWithinAt f s x) : Tendsto f (𝓝[s] x) (𝓝[f '' s] f x) :=
  h.tendsto_nhdsWithin (mapsTo_image _ _)

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