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 #

TODO #

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.

Equations
Instances For
    @[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} :
    theorem Multiset.sym2_cons {α : Type u_1} (a : α) (m : Multiset α) :
    (a ::ₘ m).sym2 = Multiset.map (fun (b : α) => s(a, b)) (a ::ₘ m) + m.sym2
    theorem Multiset.sym2_map {α : Type u_1} {β : Type u_2} (f : αβ) (m : Multiset α) :
    (Multiset.map f m).sym2 = Multiset.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 yz, 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
    theorem Multiset.dedup_sym2 {α : Type u_1} [DecidableEq α] (m : Multiset α) :
    m.sym2.dedup = m.dedup.sym2