fderiv_zero_of_not_differentiableAt

English

If f is not differentiable at x, then the Fréchet derivative fderiv 𝕜 f x is zero.

Русский

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

LaTeX

$$$$\\neg \\text{DifferentiableAt } 𝕜 f x \\implies fderiv\\ 𝕜 f x = 0.$$$$

Lean4

theorem fderiv_zero_of_not_differentiableAt (h : ¬DifferentiableAt 𝕜 f x) : fderiv 𝕜 f x = 0 :=
  by
  rw [fderiv, fderivWithin_zero_of_not_differentiableWithinAt]
  rwa [differentiableWithinAt_univ]

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