tendsto — Mathlib

English

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

Русский

Если функция f непрерывна в рамках s в точке x, то она стремится к f(x) в окрестности nhdsWithin x на s.

LaTeX

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

Lean4

/-- If a function is continuous within `s` at `x`, then it tends to `f x` within `s` by definition.
We register this fact for use with the dot notation, especially to use `Filter.Tendsto.comp` as
`ContinuousWithinAt.comp` will have a different meaning. -/
theorem tendsto (h : ContinuousWithinAt f s x) : Tendsto f (𝓝[s] x) (𝓝 (f x)) :=
  h

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