English
The list obtained by taking, for each n ≤ length(l), all sublists of length n from l, arranged over the natural numbers up to length(l), is a permutation of the sublists' of l.
Русский
Список, полученный перебором длин подсписков от 0 до длины l, упорядоченных по естественному порядку, является перестановкой подсписков l.
LaTeX
$$$$ \\bigl(\\mathrm{range}(\\mathrm{length}(l) + 1) \\;\\mathrm{flatMap} \\; (\\lambda n. \\mathrm{sublistsLen}\\ n\\; l)\\bigr) \\;\\sim \\; \\mathrm{sublists}'\\; l $$$$
Lean4
theorem range_bind_sublistsLen_perm (l : List α) :
((List.range (l.length + 1)).flatMap fun n => sublistsLen n l) ~ sublists' l := by
induction l with
| nil => simp [range_succ]
| cons h tl
l_ih =>
simp_rw [range_succ_eq_map, length, flatMap_cons, flatMap_map, sublistsLen_succ_cons, sublists'_cons,
List.sublistsLen_zero, List.singleton_append]
refine ((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_
simp_rw [← List.map_flatMap, ← cons_append]
rw [← List.singleton_append, ← List.sublistsLen_zero tl]
refine Perm.append ?_ (l_ih.map _)
rw [List.range_succ, flatMap_append, flatMap_singleton, sublistsLen_of_length_lt (Nat.lt_succ_self _), append_nil, ←
List.flatMap_map Nat.succ fun n => sublistsLen n tl, ← flatMap_cons (f := fun n => sublistsLen n tl), ←
range_succ_eq_map]
exact l_ih
