hasDerivAt_iff_tendsto_slope — Mathlib

English

If HasDerivAt f f' x, then slope f x tends to f' from both left and right directions.

Русский

Если у f в точке x существует производная f', то наклон slope f x сходится к f' слева и справа.

LaTeX

$$$\\mathrm{HasDerivAt}(f,f',x) \\Rightarrow (\\mathrm{Tendsto}\\,(\\mathrm{slope}\,f\,x)\n (\\mathcal{N}_s)\\, f')$$$

Lean4

theorem hasDerivAt_iff_tendsto_slope : HasDerivAt f f' x ↔ Tendsto (slope f x) (𝓝[≠] x) (𝓝 f') :=
  hasDerivAtFilter_iff_tendsto_slope

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