differentiableAt_of_isInvertible_fderiv

English

If the derivative fderiv 𝕜 f x is invertible as a linear map, then f is differentiable at x.

Русский

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

LaTeX

$$$\big( fderiv 𝕜 f x \big).IsInvertible \rightarrow \text{DifferentiableAt } 𝕜 f x$$$

Lean4

theorem differentiableAt_of_isInvertible_fderiv (hf : (fderiv 𝕜 f x).IsInvertible) : DifferentiableAt 𝕜 f x :=
  by
  simp only [← differentiableWithinAt_univ, ← fderivWithin_univ] at hf ⊢
  exact differentiableWithinAt_of_isInvertible_fderivWithin hf

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