tendsto_slope_zero_left — Mathlib

English

If h has a derivative at x, then the slope tends to f' from the left 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_left [Preorder 𝕜] (h : HasDerivAt f f' x) :
    Tendsto (fun t ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[<] 0) (𝓝 f') :=
  h.tendsto_slope_zero.mono_left (nhdsLT_le_nhdsNE 0)

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