sublists_cons — Mathlib

English

sublists' (a :: l) equals sublists' l concatenated with map (cons a) over sublists' l.

Русский

sublists' (a :: l) = sublists' l ⊕ map (cons a) (sublists' l).

LaTeX

$$$\\text{sublists'}(a :: l) = \\text{sublists'}(l) \\;>>=\\; (\\\\lambda x. [x, a :: x])$$$

Lean4

theorem sublists_cons (a : α) (l : List α) : sublists (a :: l) = sublists l >>= (fun x => [x, a :: x]) :=
  show sublists ([a] ++ l) = _ by
    rw [sublists_append]
    simp only [sublists_singleton, map_cons, bind_eq_flatMap, nil_append, cons_append, map_nil]

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