powersetAux_perm_powersetAux' — Mathlib

English

For any α, the two multisets powersetAux(l) and powersetAux'(l) are permutations of each other; they enumerate the same submultisets of l up to order.

Русский

Для любого l два мультимножества powersetAux(l) и powersetAux'(l) являются перестановками друг друга; они перечисляют одни и те же подмультимножества l, без учета порядка.

LaTeX

$$$ \\mathrm{powersetAux}(l) \\sim \\mathrm{powersetAux}'(l) $$$

Lean4

theorem powersetAux_perm_powersetAux' {l : List α} : powersetAux l ~ powersetAux' l := by rw [powersetAux_eq_map_coe];
  exact (sublists_perm_sublists' _).map _

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