English
If a function f has a strict derivative f' at a point and f' ≠ 0, then the corresponding inverse derivative exists as a strict Fréchet derivative via a unit automorphism.
Русский
Если функция f имеет строгую производную f' в некоторой точке и f' ≠ 0, тогда существование обратной строго-дифференцируемой производной выводится через единичную автоморфизмную структуру.
LaTeX
$$$ \\forall f, f': \\mathbb{K} \\to \\mathbb{K}, \; \\text{HasStrictDerivAt } f f' x \land f' \\neq 0 \\Rightarrow \\mathrm{HasStrictFDerivAt } f {\\(\\text{unitsEquivAut}(f')\\)} x $$$
Lean4
theorem hasFDerivAt_equiv {f : 𝕜 → 𝕜} {f' x : 𝕜} (hf : HasDerivAt f f' x) (hf' : f' ≠ 0) :
HasFDerivAt f (ContinuousLinearEquiv.unitsEquivAut 𝕜 (Units.mk0 f' hf') : 𝕜 →L[𝕜] 𝕜) x :=
hf
