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

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

@[simp]

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

@[simp]

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

theorem Multiset.mk_mem_sym2_iff {α : Type u_1} {m : Multiset α} {a : α} {b : α} : s(a, b) ∈ m.sym2 ↔ a ∈ m ∧ b ∈ m

theorem Multiset.mem_sym2_iff {α : Type u_1} {m : Multiset α} {z : Sym2 α} : z ∈ m.sym2 ↔ ∀ y ∈ z, y ∈ m

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

@[simp]

theorem Multiset.sym2_mono {α : Type u_1} {m : Multiset α} {m' : Multiset α} (h : m ≤ m') : m.sym2 ≤ m'.sym2

theorem Multiset.monotone_sym2 {α : Type u_1} : Monotone Multiset.sym2

theorem Multiset.card_sym2 {α : Type u_1} {m : Multiset α} : Multiset.card m.sym2 = (Multiset.card m + 1).choose 2