toHomeomorph_toEquiv — Mathlib

English

For a given diffeomorphism h, the underlying equivalence of its associated homeomorphism matches the original equivalence of h.

Русский

Для данного диффеоморфа h соответствующее тождественное отображение гомеоморфизма имеет ту же базовую эквивалентность, что и сама h.

LaTeX

$$$h^{\\text{toHomeomorph}}.toEquiv = h.toEquiv$$$

Lean4

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

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