symm_comp_self

Mathlib.Order.RelIso.Basic

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

English

The composition of a RelIso with its inverse is the identity: e.symm ∘ e = id.

Русский

Скрещивание RelIso с его обратным приводит к тождественной функции: e.symm ∘ e = id.

LaTeX

$$$$ e^{\\mathrm{symm}} \\circ e = \\mathrm{id}. $$$$

Lean4

@[simp]
theorem symm_comp_self (e : r ≃r s) : e.symm ∘ e = id :=
  funext e.symm_apply_apply

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

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

Разделы

Аффилиация

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