trans_eq_refl_iff_symm_eq

Mathlib.Logic.Equiv.Defs

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

← MathLib Explorer

English

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

Русский

Для f: α ≃ β и g: β ≃ α, f.trans g = Id ↔ f.symm = g.

LaTeX

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

Lean4

theorem trans_eq_refl_iff_symm_eq {f : α ≃ β} {g : β ≃ α} : f.trans g = Equiv.refl α ↔ f.symm = g :=
  by
  rw [trans_eq_refl_iff_eq_symm]
  exact ⟨fun h ↦ h ▸ rfl, fun h ↦ h ▸ rfl⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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