Documentation

Mathlib.Data.Multiset.Sort

Construct a sorted list from a multiset. #

def Multiset.sort {α : Type u_1} (r : ααProp) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (s : Multiset α) :
List α

sort s constructs a sorted list from the multiset s. (Uses merge sort algorithm.)

Equations
Instances For
    @[simp]
    theorem Multiset.coe_sort {α : Type u_1} (r : ααProp) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (l : List α) :
    @[simp]
    theorem Multiset.sort_sorted {α : Type u_1} (r : ααProp) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (s : Multiset α) :
    @[simp]
    theorem Multiset.sort_eq {α : Type u_1} (r : ααProp) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (s : Multiset α) :
    (Multiset.sort r s) = s
    @[simp]
    theorem Multiset.mem_sort {α : Type u_1} (r : ααProp) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] {s : Multiset α} {a : α} :
    @[simp]
    theorem Multiset.length_sort {α : Type u_1} (r : ααProp) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] {s : Multiset α} :
    (Multiset.sort r s).length = Multiset.card s
    @[simp]
    theorem Multiset.sort_zero {α : Type u_1} (r : ααProp) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] :
    @[simp]
    theorem Multiset.sort_singleton {α : Type u_1} (r : ααProp) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (a : α) :
    Multiset.sort r {a} = [a]
    theorem Multiset.map_sort {α : Type u_1} {β : Type u_2} (r : ααProp) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (r' : ββProp) [DecidableRel r'] [IsTrans β r'] [IsAntisymm β r'] [IsTotal β r'] (f : αβ) (s : Multiset α) (hs : as, bs, r a b r' (f a) (f b)) :
    theorem Multiset.sort_cons {α : Type u_1} (r : ααProp) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (a : α) (s : Multiset α) :
    (∀ bs, r a b)Multiset.sort r (a ::ₘ s) = a :: Multiset.sort r s
    unsafe instance Multiset.instRepr {α : Type u_1} [Repr α] :