tendsto_nhds — Mathlib

English

If L ≤ 𝓝 x and f has a derivative at x with respect to L, then f tends to f(x) along L.

Русский

Если L ≤ 𝓝 x и f имеет производную относительно фильтра L в точке x, то f сходится к f(x) вдоль L.

LaTeX

$$$L \\leq \\mathcal{N}(x) \\;\\wedge\\; \\text{HasDerivAtFilter } f\\ f'\\ x\\ L \\Rightarrow \\operatorname{Tendsto} f\\ L\\ \\mathcal{N}(f(x)).$$$

Lean4

nonrec theorem tendsto_nhds (hL : L ≤ 𝓝 x) (h : HasDerivAtFilter f f' x L) : Tendsto f L (𝓝 (f x)) :=
  h.tendsto_nhds hL

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