iff_reverse_eq

Mathlib.Data.List.Palindrome

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

English

If reverse l equals l, then l is a palindrome.

Русский

Если обращение списка равно списку, то список является палиндромом.

LaTeX

$$$\\operatorname{reverse}(l) = l \\Rightarrow \\operatorname{Palindrome}(l).$$$

Lean4

theorem iff_reverse_eq {l : List α} : Palindrome l ↔ reverse l = l :=
  Iff.intro reverse_eq of_reverse_eq

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

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

Разделы

Аффилиация

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