map — Mathlib

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]

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