sublistsLen_one — Mathlib

English

For any list l, the sublists of length 1 are the singleton elements of l in reverse order.

Русский

Для списка l подсписки длины 1 образуют одинарные списки элементов l в обратном порядке.

LaTeX

$$$\\operatorname{sublistsLen}(1, l) = \\operatorname{reverse}(l).map ([\\cdot])$$$

Lean4

theorem sublistsLen_one (l : List α) : sublistsLen 1 l = l.reverse.map ([·]) :=
  l.rec (by rw [sublistsLen_succ_nil, reverse_nil, map_nil]) fun a s ih ↦ by
    rw [sublistsLen_succ_cons, ih, reverse_cons, map_append, sublistsLen_zero]; rfl

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