map_reverse_tails — Mathlib

English

For any list l, mapping reverse on l.tails equals the reverse of the inits of reverse l, i.e. map(reverse)(l.tails) = reverse(inits(reverse l)).

Русский

Для списка l отображение reverse на l.tails равно reverse(inits(reverse l)).

LaTeX

$$$\\operatorname{map}(\\operatorname{reverse}, \\operatorname{tails}(l)) = \\operatorname{reverse}(\\operatorname{inits}(\\operatorname{reverse}(l)))$$$

Lean4

theorem map_reverse_tails (l : List α) : map reverse l.tails = (reverse <| inits <| reverse l) :=
  by
  rw [tails_eq_inits l]
  simp [← map_reverse]

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