powersetAux'_cons — Mathlib

English

For any a and list l, the submultiset collection of a appended to l equals the submultisets of l plus those obtained by cons a to each submultiset of l.

Русский

Для любого элемента a и списка l множество подмультимножеств, получаемое добавлением a в начало, равно сумме подмультимножеств l и тех, которые получаются применением конструирования cons a к каждому подмультимножесту l.

LaTeX

$$$ \\mathrm{powersetAux}'(a:\\,l) = \\mathrm{powersetAux}'(l) + \\mathrm{map}(\\mathrm{cons}\\ a)\\big(\\mathrm{powersetAux}'(l)\\big) $$$

Lean4

@[simp]
theorem powersetAux'_cons (a : α) (l : List α) :
    powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l) := by simp [powersetAux']

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