English
There exists a local inverse around x for a local diffeomorphism.
Русский
Существет локальный обратный вокруг точки x для локального диффеоморфизма.
LaTeX
$$∃ Φ : PartialDiffeomorph I J n f x, IsLocalDiffeomorphAt I J n f x$$
Lean4
/-- The inverse of a local diffeomorphism. -/
protected def symm : PartialDiffeomorph J I N M n
where
toPartialEquiv := Φ.toPartialEquiv.symm
open_source := Φ.open_target
open_target := Φ.open_source
contMDiffOn_toFun := Φ.contMDiffOn_invFun
contMDiffOn_invFun := Φ.contMDiffOn_toFun