symm_eq_self_of_involutive

Mathlib.Logic.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#Function.Involutive.symm_eq_self_of_involutive

English

If a permutation f is involutive, then its inverse equals itself: f^{-1} = f.

Русский

Если перестановка f инволютивна, то её обратное равняется самой f: f^{-1} = f.

LaTeX

$$f^{-1} = f$$

Lean4

theorem symm_eq_self_of_involutive (f : Equiv.Perm α) (h : Involutive f) : f.symm = f :=
  DFunLike.coe_injective (h.leftInverse_iff.mp f.left_inv)

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

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

Разделы

Аффилиация

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