coe_toPerm

Mathlib.Logic.Equiv.Basic

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

English

For an involutive function h, the underlying function of h.toPerm f is f.

Русский

Для инволютной функции h основанная функция h.toPerm f равна f.

LaTeX

$$(h.toPerm f)(x) = f(x)$$

Lean4

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

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

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

Разделы

Аффилиация

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