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 α} :
    List.length (Multiset.sort r s) = 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]
    unsafe instance Multiset.instReprMultiset {α : Type u_1} [Repr α] :
    Equations
    • One or more equations did not get rendered due to their size.