powerset_coe — Mathlib

English

The powerset of a list l, regarded as a multiset, equals the multiset of the images of all sublists of l under the natural coercion to multisets.

Русский

Множество подмножеств списка (как мультимножество) равно мультимножеству образов всех подсписков l под естественным преобразованием в мультимножества.

LaTeX

$$$ \\mathrm{powerset}(l) = \\big(\\mathrm{sublists}(l)\\big) \\mapsto (\\uparrow) $$$

Lean4

theorem powerset_coe (l : List α) : @powerset α l = ((sublists l).map (↑) : List (Multiset α)) :=
  congr_arg ((↑) : List (Multiset α) → Multiset (Multiset α)) powersetAux_eq_map_coe

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