append_reverse

Mathlib.Data.List.Palindrome

URI: https://scilib.ai/kg/mathlib#List.Palindrome.append_reverse

English

For any list l, the concatenation l ++ reverse l is a palindrome.

Русский

Для любого списка l конкатенация l ++ reverse(l) является палиндромом.

LaTeX

$$$\\operatorname{Palindrome}(l \\;\\oplus\\; \\operatorname{reverse}(l)).$$$

Lean4

theorem append_reverse (l : List α) : Palindrome (l ++ reverse l) :=
  by
  apply of_reverse_eq
  rw [reverse_append, reverse_reverse]

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

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

Разделы

Аффилиация

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