sublists_concat — Mathlib

English

sublists (l ++ [a]) equals sublists l concatenated with map (λ x, x ++ [a]) (sublists l).

Русский

sublists (l ++ [a]) = sublists l ⊕ map (λ x, x ++ [a]) (sublists l).

LaTeX

$$$\\text{sublists}(l ++ [a]) = \\text{sublists}(l) >>= (\\\\lambda x. \\text{map} (\\\\lambda y. y ++ [a]) x)$$$

Lean4

@[simp]
theorem sublists_concat (l : List α) (a : α) :
    sublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l) := by
  rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
    map_id'' append_nil, append_nil]

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