sublistsLen — Mathlib

English

The list of all sublists of length n of a list l is defined by sublistsLen n l = sublistsLenAux n l id [].

Русский

Список всех подсписков длины n списка l задаётся как sublistsLen n l = sublistsLenAux n l id [].

LaTeX

$$$\\operatorname{sublistsLen}(n, l) = \\operatorname{sublistsLenAux}(n, l, \\mathrm{id}, [])$$$

Lean4

/-- The list of all sublists of a list `l` that are of length `n`. For instance, for
`l = [0, 1, 2, 3]` and `n = 2`, one gets
`[[2, 3], [1, 3], [1, 2], [0, 3], [0, 2], [0, 1]]`. -/
def sublistsLen (n : ℕ) (l : List α) : List (List α) :=
  sublistsLenAux n l id []

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