hasFDerivAt — Mathlib

English

If f is strictly differentiable at x with derivative f', then f is differentiable at x with derivative f'.

Русский

Если f строго дифференцируема в точке x с производной f', то в точке x функция имеет обыкновенную производную с той же производной f'.

LaTeX

$$$ \\text{If } \\text{HasStrictFDerivAt } f\\ f'\\ x, \\text{ then } \\text{HasFDerivAt } f\\ f'\\ x. $$$$

Lean4

@[fun_prop]
protected theorem hasFDerivAt (hf : HasStrictFDerivAt f f' x) : HasFDerivAt f f' x :=
  .of_isLittleOTVS <| by simpa only using hf.isLittleOTVS.comp_tendsto (tendsto_id.prodMk_nhds tendsto_const_nhds)

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