symm — Mathlib

English

The inverse of the inverse of a C^n-diffeomorphism is the original diffeomorphism.

Русский

Обратная к обратной диффеоморфизм — это сам исходный диффеоморфизм.

LaTeX

$$$(h^{-1})^{-1} = h,$ where $h$ is a C^n-diffeomorphism.$$

Lean4

/-- Inverse of a diffeomorphism. -/
@[symm]
protected def symm (h : M ≃ₘ^n⟮I, J⟯ N) : N ≃ₘ^n⟮J, I⟯ M
    where
  contMDiff_toFun := h.contMDiff_invFun
  contMDiff_invFun := h.contMDiff_toFun
  toEquiv := h.toEquiv.symm

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