symm_eq_iff_trans_eq_refl

Mathlib.Logic.Equiv.Defs

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

English

For f: α ≃ β and g: β ≃ α, f.symm = g iff f.trans g = Id.

Русский

Для f: α ≃ β и g: β ≃ α, f.symm = g тогда и только тогда, когда f.trans g = Id.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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