sublistsLenAux_eq — Mathlib

English

For all n, l, f, r, the auxiliary function equals the map of f over sublists of length n, concatenated with r.

Русский

Для любых n, l, f, r вспомогательная функция равна отображению f над подсписками длины n, конкатенированному с r.

LaTeX

$$$\\operatorname{sublistsLenAux}(n, l, f, r) = (\\operatorname{sublistsLen}(n, l)).map f ++ r$$$

Lean4

theorem sublistsLenAux_eq (l : List α) (n) (f : List α → β) (r) :
    sublistsLenAux n l f r = (sublistsLen n l).map f ++ r := by rw [sublistsLen, ← sublistsLenAux_append]; rfl

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