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 : Multiset α) : Multiset (Sym2 α)

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

• Multiset.sym2 m = Quotient.liftOn m (fun (xs : List α) => ↑(List.sym2 xs)) ⋯

@[simp]

theorem Multiset.sym2_coe {α : Type u_1} (xs : List α) : Multiset.sym2 ↑xs = ↑(List.sym2 xs)

@[simp]

theorem Multiset.sym2_eq_zero_iff {α : Type u_1} {m : Multiset α} : Multiset.sym2 m = 0 ↔ m = 0

theorem Multiset.mk_mem_sym2_iff {α : Type u_1} {m : Multiset α} {a : α} {b : α} : s(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 ↔ ∀ y ∈ z, y ∈ m

theorem Multiset.Nodup.sym2 {α : Type u_1} {m : Multiset α} (h : Multiset.Nodup m) : Multiset.Nodup (Multiset.sym2 m)

@[simp]

theorem Multiset.sym2_mono {α : Type u_1} {m : Multiset α} {m' : Multiset α} (h : m ≤ m') : Multiset.sym2 m ≤ Multiset.sym2 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