toPerm_symm

Mathlib.Logic.Equiv.Basic

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

English

The inverse of the permutation h.toPerm f is equal to h.toPerm f itself.

Русский

Обратная к перестановке h.toPerm f равна самой перестановке.

LaTeX

$$(h.toPerm f)^{-1} = h.toPerm f$$

Lean4

@[simp]
theorem toPerm_symm {f : α → α} (h : Involutive f) : (h.toPerm f).symm = h.toPerm f :=
  rfl

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

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

Разделы

Аффилиация

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