symm_toHomeomorph — Mathlib

English

The symmetry (inverse) of the homeomorphism induced by a diffeomorphism equals the image under the symmetry of the original diffeomorphism.

Русский

Обратное отображение, индуцированное гомеоморфизмом, совпадает с образом симметрии исходного диффеоморфизма.

LaTeX

$$$h^{\\text{symm}}^{\\text{toHomeomorph}} = h^{\\text{toHomeomorph}}^{\\text{symm}}$$$

Lean4

@[simp]
theorem symm_toHomeomorph (h : M ≃ₘ^n⟮I, J⟯ N) : h.symm.toHomeomorph = h.toHomeomorph.symm :=
  rfl

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