differentiableWithinAt_of_isInvertible_fderivWithin

English

If the restricted derivative fderivWithin 𝕜 f s x exists and is invertible as a continuous linear map, then f is differentiable within s at x.

Русский

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

LaTeX

$$$\big( (fderivWithin 𝕜 f s x).IsInvertible \big) \rightarrow \text{DifferentiableWithinAt } 𝕜 f s x$$$

Lean4

theorem differentiableWithinAt_of_isInvertible_fderivWithin (hf : (fderivWithin 𝕜 f s x).IsInvertible) :
    DifferentiableWithinAt 𝕜 f s x := by
  contrapose hf
  rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
  contrapose! hf
  rcases isInvertible_zero_iff.1 hf with ⟨hE, hF⟩
  exact (hasFDerivAt_of_subsingleton _ _).differentiableAt.differentiableWithinAt

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