not_differentiableAt_of_local_left_inverse_hasDerivAt_zero

English

If the local left inverse fails differentiability, the inverse construction cannot yield a derivative.

Русский

Если локальная левая обратная функция не дифференцируема, вывод о существовании производной не выполняется.

LaTeX

$$$ (\\text{conditions}) \\Rightarrow \\neg \\mathrm{HasDerivAt} g a $$$

Lean4

theorem not_differentiableAt_of_local_left_inverse_hasDerivAt_zero {f g : 𝕜 → 𝕜} {a : 𝕜} (hf : HasDerivAt f 0 (g a))
    (hfg : f ∘ g =ᶠ[𝓝 a] id) : ¬DifferentiableAt 𝕜 g a :=
  by
  intro hg
  have := (hf.comp a hg.hasDerivAt).congr_of_eventuallyEq hfg.symm
  simpa using this.unique (hasDerivAt_id a)

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