localInverse — Mathlib

English

If a local inverse exists, its mapping is differentiable on the target.

Русский

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

LaTeX

$$IsLocalDiffeomorphAt I J n f x \Rightarrow ContMDiffAt J I n (hf.localInverse) x$$

Lean4

/-- An arbitrary choice of local inverse of `f` near `x`. -/
noncomputable def localInverse (hf : IsLocalDiffeomorphAt I J n f x) : PartialDiffeomorph J I N M n :=
  (Classical.choose hf).symm

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