powerset_coe' — Mathlib

English

The powerset of a list l is, up to equality, the same as the image of sublists' under the multiset-coercion.

Русский

Множество подмножеств списка эквивалентно по равенству образу подсписков l под операцией приведения к мультимножествах.

LaTeX

$$$ \\mathrm{powerset}(l) = (\\mathrm{sublists}'(l)).map(\\uparrow)$$$

Lean4

@[simp]
theorem powerset_coe' (l : List α) : @powerset α l = ((sublists' l).map (↑) : List (Multiset α)) :=
  Quot.sound powersetAux_perm_powersetAux'

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