localInverse_contMDiffAt — Mathlib

English

Let f be a C^n local diffeomorphism at x; then the local inverse of f is C^n-differentiable at f(x).

Русский

Пусть f является локальным диффеоморфизмом класса C^n в точке x; тогда локальный обратный отображение f гладко дифференцируемо класса C^n в точке f(x).

LaTeX

$$$ ContMDiffAt J I n\; hf.localInverse\; (f\,x) $$$

Lean4

theorem localInverse_contMDiffAt (hf : IsLocalDiffeomorphAt I J n f x) : ContMDiffAt J I n hf.localInverse (f x) :=
  hf.localInverse_contMDiffOn.contMDiffAt (hf.localInverse.open_source.mem_nhds hf.localInverse_mem_source)

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