symm — Mathlib

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

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