powersetCardAux — Mathlib

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 (↑) []

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