map_reverse_inits — Mathlib

English

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

Русский

Для любого списка l отображение reverse на l.inits равно обратному хвостам обратного списка l: map(reverse)(l.inits) = reverse(tails(reverse l)).

LaTeX

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

Lean4

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

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