Documentation

Mathlib.Data.Multiset.Sym

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 #

• Multiset.sym2: xs.sym2 is the multiset of all unordered pairs of elements from xs, with multiplicity. The multiset's values are in Sym2 α.

TODO #

• Once List.Perm.sym is defined, define

protected def sym (n : Nat) (m : Multiset α) : Multiset (Sym α n) :=
m.liftOn (fun xs => xs.sym n) (List.perm.sym n)


and then use this to remove the DecidableEq assumption from Finset.sym.

• theorem injective_sym2 : Function.Injective (Multiset.sym2 : Multiset α → _)

• theorem strictMono_sym2 : StrictMono (Multiset.sym2 : Multiset α → _)

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

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.

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