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

@[simp]

theorem Multiset.sym2_zero {α : Type u_1} : Multiset.sym2 0 = 0

theorem Multiset.sym2_cons {α : Type u_1} (a : α) (m : Multiset α) : (a ::ₘ m).sym2 = map (fun (b : α) => s(a, b)) (a ::ₘ m) + m.sym2

theorem Multiset.sym2_map {α : Type u_1} {β : Type u_2} (f : α → β) (m : Multiset α) : (map f m).sym2 = map (Sym2.map f) m.sym2

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.setOf_mem_sym2 {α : Type u_1} {m : Multiset α} : {z : Sym2 α | z ∈ m.sym2} = {x : α | x ∈ m}.sym2

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

@[simp]

theorem Multiset.sym2_mono {α : Type u_1} {m 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 α} : m.sym2.card = (m.card + 1).choose 2

theorem Multiset.dedup_sym2 {α : Type u_1} [DecidableEq α] (m : Multiset α) : m.sym2.dedup = m.dedup.sym2