tendsto_slope_zero_right — Mathlib

English

If h has a derivative at x, then the slope tends to f' from the right as t → 0+.

Русский

Если у h существует производная в точке x, то наклон стремится к производной справа при t → 0+.

LaTeX

$$$\\mathrm{HasDerivAt}(f,f',x) \\Rightarrow \\mathrm{Tendsto}\\left( t \\mapsto t^{-1}(f(x+t)-f(x))\\right)\\left(\\mathcal{N}_{0}^{>}\n\\right)(\\mathcal{N} f')$$$

Lean4

theorem tendsto_slope_zero_right [Preorder 𝕜] (h : HasDerivAt f f' x) :
    Tendsto (fun t ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[>] 0) (𝓝 f') :=
  h.tendsto_slope_zero.mono_left (nhdsGT_le_nhdsNE 0)

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