English
Let l be a list. The tails of the reverse of l are exactly the reverse of the images under reverse of the inits of l, i.e. tails(reverse l) = reverse(map(reverse)(l.inits)).
Русский
Пусть l — конечный список. Хвосты списка reverse(l) равны обратному отображению списка начальных префиксов l: tails(reverse(l)) = reverse(map(reverse)(l.inits)).
LaTeX
$$$\\operatorname{tails}(\\operatorname{reverse}(l)) = \\operatorname{reverse}(\\operatorname{map}(\\operatorname{reverse})(\\operatorname{inits}(l)))$$$
Lean4
theorem tails_reverse (l : List α) : tails (reverse l) = reverse (map reverse l.inits) :=
by
rw [inits_eq_tails l]
simp [← map_reverse]
