toEquiv_inj

Mathlib.Topology.MetricSpace.Isometry

URI: https://scilib.ai/kg/mathlib#IsometryEquiv.toEquiv_inj

English

If e1.toEquiv = e2.toEquiv for isotropy, then e1 = e2.

Русский

Если e1.toEquiv = e2.toEquiv, то e1 = e2.

LaTeX

$$$ (e_1.toEquiv = e_2.toEquiv) \iff e_1 = e_2. $$$

Lean4

@[simp]
theorem toEquiv_inj {e₁ e₂ : α ≃ᵢ β} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂ :=
  toEquiv_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru