differentiableAt_of_deriv_ne_zero

Mathlib.Analysis.Calculus.Deriv.Basic

URI: https://scilib.ai/kg/mathlib#differentiableAt_of_deriv_ne_zero

English

If deriv f x ≠ 0, then f is differentiable at x.

Русский

Если производная deriv f x не ноль, значит функция дифференцируема в точке x.

LaTeX

$$$\\operatorname{deriv} f x \\neq 0 \\Rightarrow \\operatorname{DifferentiableAt}_{\\mathbb{K}}(f,x).$$$

Lean4

theorem differentiableAt_of_deriv_ne_zero (h : deriv f x ≠ 0) : DifferentiableAt 𝕜 f x :=
  not_imp_comm.1 deriv_zero_of_not_differentiableAt h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru