tendsto_slope_zero_right — Mathlib

English

From HasLineDerivAt, the right-hand slope tends to the derivative as t → 0+.

Русский

Из HasLineDerivAt следует, что вправо предел скорости умеет совпасть с производной при t → 0+.

LaTeX

$$$\text{HasLineDerivAt}_{\mathbb{k}}(f,f',x,v) \Rightarrow \mathrm{Tendsto}(t \mapsto t^{-1}(f(x+t v)-f(x)), (0,\infty), f')$$$

Lean4

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

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