powersetCard — Mathlib

English

As above: permutation invariance of powersetCardAux under list permutation.

Русский

Как выше: перестановочная инварианта PowersetCardAux при перестановке списка.

LaTeX

$$l.Perm l' → (powersetCardAux n l).Perm (powersetCardAux n l')$$

Lean4

/-- `powersetCard n s` is the multiset of all submultisets of `s` of length `n`. -/
def powersetCard (n : ℕ) (s : Multiset α) : Multiset (Multiset α) :=
  Quot.liftOn s (fun l => (powersetCardAux n l : Multiset (Multiset α))) fun _ _ h =>
    Quot.sound (powersetCardAux_perm h)

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