reverse_reverse

Mathlib.Combinatorics.Enumerative.Composition

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

English

Applying reversal twice yields the original composition.

Русский

Применение разворота дважды дает исходную композицию.

LaTeX

$$$\\forall c:\\, \\mathrm{Composition}(n),\\ \\mathrm{reverse}(\\mathrm{reverse}(c)) = c.$$$

Lean4

@[simp]
theorem reverse_reverse (c : Composition n) : c.reverse.reverse = c :=
  Composition.ext <| List.reverse_reverse _

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

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

Разделы

Аффилиация

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