differentiableWithinAt_of_derivWithin_ne_zero

English

If derivWithin f s x ≠ 0, then f is differentiable within at s at x.

Русский

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

LaTeX

$$$\\bigl( \\operatorname{derivWithin} f\\ s\\ x \\neq 0 \\bigr) \\Rightarrow \\operatorname{DifferentiableWithinAt}_{\\mathbb{K}}(f,s,x).$$$

Lean4

theorem differentiableWithinAt_of_derivWithin_ne_zero (h : derivWithin f s x ≠ 0) : DifferentiableWithinAt 𝕜 f s x :=
  not_imp_comm.1 derivWithin_zero_of_not_differentiableWithinAt h

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