powersetCard_coe — Mathlib

English

For any n and list l, powersetCard n (ofList l) equals ofList (powersetCardAux n l).

Русский

Для любого n и списка l, powersetCard n (ofList l) эквивалентно ofList (powersetCardAux n l).

LaTeX

$$powersetCard(n, \\mathrm{ofList}(l)) = \\mathrm{ofList}(powersetCardAux(n, l))$$

Lean4

theorem powersetCard_coe (n) (l : List α) : @powersetCard α n l = ((sublistsLen n l).map (↑) : List (Multiset α)) :=
  congr_arg ((↑) : List (Multiset α) → Multiset (Multiset α)) powersetCardAux_eq_map_coe

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