English
powersetCardAux(n, l) is the list of submultisets of l of length n, represented as multisets.
Русский
powersetCardAux(n, l) — это список подмультимножеств l длины n, представленных как мультимножества.
LaTeX
$$powersetCardAux(n, l) = List of multisets corresponding to sublists of length n from l$$
Lean4
/-- Helper function for `powersetCard`. Given a list `l`, `powersetCardAux n l` is the list
of sublists of length `n`, as multisets. -/
def powersetCardAux (n : ℕ) (l : List α) : List (Multiset α) :=
sublistsLenAux n l (↑) []