sublists'_cons — Mathlib

English

For any a and l, sublists'(a :: l) equals sublists'(l) concatenated with map (cons a) (sublists'(l)).

Русский

Для любого элемента a и списка l выполняется: sublists'(a :: l) = sublists'(l) ++ map (cons a) (sublists'(l)).

LaTeX

$$$\\mathrm{sublists}'(a \\;::\\; l) = \\mathrm{sublists}' l \\;++\\; \\mathrm{map} (\\mathrm{cons} \\ a)\\ (\\mathrm{sublists}' l)$$$

Lean4

@[simp 900]
theorem sublists'_cons (a : α) (l : List α) : sublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l) := by
  simp [sublists'_eq_sublists'Aux, foldr_cons, sublists'Aux_eq_map]

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