contmdiffOn_localInverse — Mathlib

English

If f is locally a diffeomorphism, then its local inverse is ContMDiffOn on its domain.

Русский

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

LaTeX

$$$$ \text{ContMDiffOn}(J,I,n, \text{hf.localInverse}, \text{hf.localInverse.source}). $$$$

Lean4

theorem contmdiffOn_localInverse (hf : IsLocalDiffeomorphAt I J n f x) :
    ContMDiffOn J I n hf.localInverse hf.localInverse.source :=
  hf.localInverse.contMDiffOn_toFun

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