deriv_zero_of_not_differentiableAt

English

If f is not differentiable at x, then deriv f x = 0.

Русский

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

LaTeX

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

Lean4

theorem deriv_zero_of_not_differentiableAt (h : ¬DifferentiableAt 𝕜 f x) : deriv f x = 0 :=
  by
  unfold deriv
  rw [fderiv_zero_of_not_differentiableAt h]
  simp

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