symm_trans_self

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.symm_trans_self

English

For e : α ≃ β, the inverse followed by the forward map yields the identity on β: e.symm.trans e = Equiv.refl β.

Русский

Для e : α ≃ β обратная карта следует за прямой: e.symm.trans e = Equiv.refl β.

LaTeX

$$$e.symm.trans e = Equiv.refl\\beta$$$

Lean4

@[simp]
theorem symm_trans_self (e : α ≃ β) : e.symm.trans e = Equiv.refl β := by grind

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

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

Разделы

Аффилиация

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