localInverse_mdifferentiableAt — Mathlib

English

If hf is a local diffeomorphism at x of order n, then the local inverse is MDifferentiableAt at f(x) (provided n ≥ 1).

Русский

Если hf задаёт локальный диффеоморфизм в точке x порядка n, то локальная обратная карта дифференцируема на классе MDifferentiableAt в точке f(x) (при n ≥ 1).

LaTeX

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

Lean4

theorem localInverse_mdifferentiableAt (hf : IsLocalDiffeomorphAt I J n f x) (hn : 1 ≤ n) :
    MDifferentiableAt J I hf.localInverse (f x) :=
  hf.localInverse_contMDiffAt.mdifferentiableAt hn

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