THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
list.sublists gives a list of all (not necessarily contiguous) sublists of a list.
This file contains basic results on this function.
Auxiliary function to construct the list of all sublists of a given length. Given an
n, a list
l, a function
f and an auxiliary list
L, it returns the list made of
f applied to all sublists of
l of length
n, concatenated with
- list.sublists_len_aux (n + 1) (a :: l) f r = list.sublists_len_aux (n + 1) l f (list.sublists_len_aux n l (f ∘ list.cons a) r)
- list.sublists_len_aux (n + 1) list.nil f r = r
- list.sublists_len_aux 0 (hd :: tl) f r = f list.nil :: r
- list.sublists_len_aux 0 list.nil f r = f list.nil :: r
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]].
Alias of the forward direction of
Alias of the reverse direction of