localInverse_contMDiffOn — Mathlib

English

The local inverse hf.localInverse is ContMDiffOn on its source.

Русский

Локальное обратное hf.localInverse гладко дифференцируемо на области определения.

LaTeX

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

Lean4

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

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