inits_eq_tails — Mathlib

English

For any list l, inits(l) is mapped from tails of reverse l; more precisely, l.inits = reverse (map reverse (tails (reverse l))).

Русский

Для любого списка l вершины inits(l) эквивалентны обратному отображению хвостов обратного l.

LaTeX

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

Lean4

theorem inits_eq_tails : ∀ l : List α, l.inits = (reverse <| map reverse <| tails <| reverse l)
  | [] => by simp
  | a :: l => by simp [inits_eq_tails l, map_inj_left, ← map_reverse]

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