eq_symm_iff_trans_eq_refl

Mathlib.Logic.Equiv.Defs

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

English

Equivalently, f = g.symm iff f.trans g = Id.

Русский

Эквивалентно, f = g.symm, если и только если f.trans g = Id.

LaTeX

$$$ f = g^{-1} \iff f.trans g = \mathrm{Id}_α $$$

Lean4

theorem eq_symm_iff_trans_eq_refl {f : α ≃ β} {g : β ≃ α} : f = g.symm ↔ f.trans g = Equiv.refl α :=
  trans_eq_refl_iff_eq_symm.symm

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

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

Разделы

Аффилиация

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