reverse_involutive

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#Composition.reverse_involutive

English

The reverse operation is an involution on the family of compositions: applying it twice gives the identity.

Русский

Операция разворота образует инволюцию над семейством композиций: два применения дают тождество.

LaTeX

$$$\\text{Involutive}(\\mathrm{reverse})$$$

Lean4

theorem reverse_involutive : Function.Involutive (@reverse n) :=
  reverse_reverse

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

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

Разделы

Аффилиация

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