inits_reverse — Mathlib

English

Inits of the reverse of a list correspond to reversing the tails of the original list: inits(reverse l) = reverse (map reverse l.tails).

Русский

Инициалы от развернутого списка соответствуют развороту обратных хвостов исходного списка.

LaTeX

$$$\forall l : \text{List}(\alpha),\; \text{inits}(\text{reverse } l) = \text{reverse} (\text{map reverse } l.\text{tails}).$$$

Lean4

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

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