English
If p is a palindrome on l and f is a function, then map f l is a palindrome.
Русский
Если p является палиндромом списка l и задано отображение f, то отображение f по l образует палиндром.
LaTeX
$$$\\forall f:\\alpha \\to \\beta,\\ Palindrome(l) \\Rightarrow Palindrome(\\operatorname{map}(f,l)).$$$
Lean4
protected theorem map (f : α → β) (p : Palindrome l) : Palindrome (map f l) :=
of_reverse_eq <| by rw [← map_reverse, p.reverse_eq]