toEquiv_inj — Mathlib

English

If two diffeomorphisms have the same underlying equivalence, then they are equal; thus the map h ↦ h.toEquiv is injective.

Русский

Если две диффеоморфизмы имеют одинаковое базовое эквивалентное отображение, то они равны; следовательно, отображение h ↦ h.toEquiv инъективно.

LaTeX

$$$\text{If } h,h' : M \simeq M' \text{ are diffeomorphisms of class } C^n(I,I'),\; h.toEquiv = h'.toEquiv\;\Rightarrow\; h = h'.$$$

Lean4

@[simp]
theorem toEquiv_inj {h h' : M ≃ₘ^n⟮I, I'⟯ M'} : h.toEquiv = h'.toEquiv ↔ h = h' :=
  toEquiv_injective.eq_iff

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