symm_comp_self

Mathlib.Topology.MetricSpace.Isometry

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

English

h^{-1} ∘ h = id

Русский

h.symm ∘ h = id

LaTeX

$$$ (h.symm : β\rightarrow α) \circ h = \mathrm{id}$$$

Lean4

theorem symm_comp_self (h : α ≃ᵢ β) : (h.symm : β → α) ∘ h = id :=
  funext h.left_inv

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

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

Разделы

Аффилиация

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