Unordered tuples of elements of a multiset #

Defines Multiset.sym and the specialized Multiset.sym2 for computing multisets of all unordered n-tuples from a given multiset. These are multiset versions of Nat.multichoose.

Main declarations #


def Multiset.sym2 {α : Type u_1} (m : Multiset α) :

m.sym2 is the multiset of all unordered pairs of elements from m, with multiplicity. If m has no duplicates then neither does m.sym2.

  • One or more equations did not get rendered due to their size.
Instances For
    theorem Multiset.sym2_coe {α : Type u_1} (xs : List α) :
    Multiset.sym2 xs = (List.sym2 xs)
    theorem Multiset.sym2_eq_zero_iff {α : Type u_1} {m : Multiset α} :
    theorem Multiset.mk_mem_sym2_iff {α : Type u_1} {m : Multiset α} {a : α} {b : α} :
    (a, b) Multiset.sym2 m a m b m
    theorem Multiset.mem_sym2_iff {α : Type u_1} {m : Multiset α} {z : Sym2 α} :
    z Multiset.sym2 m yz, y m
    theorem Multiset.sym2_mono {α : Type u_1} {m : Multiset α} {m' : Multiset α} (h : m m') :
    theorem Multiset.monotone_sym2 {α : Type u_1} :
    Monotone Multiset.sym2
    theorem Multiset.card_sym2 {α : Type u_1} {m : Multiset α} :
    Multiset.card (Multiset.sym2 m) = Nat.choose (Multiset.card m + 1) 2