mdifferentiable_of_subsingleton — Mathlib

English

If the mfderiv is invertible, then f is differentiable at x.

Русский

Если mfderiv обратим, то f дифференцируема в точке x.

LaTeX

$$(mfderiv I I' f x).IsInvertible → MDifferentiableAt I I' f x$$

Lean4

theorem mdifferentiable_of_subsingleton [Subsingleton E] : MDifferentiable I I' f :=
  by
  intro x
  have : Subsingleton H := I.injective.subsingleton
  have : DiscreteTopology M := discreteTopology H M
  simp only [mdifferentiableAt_iff, continuous_of_discreteTopology.continuousAt, true_and]
  exact (hasFDerivAt_of_subsingleton _ _).differentiableAt.differentiableWithinAt

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