Documentation

Mathlib.Data.Multiset.Sort

Construct a sorted list from a multiset. #

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

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

Equations
@[simp]
theorem Multiset.coe_sort {α : Type u_1} (r : ααProp) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] (l : List α) :
@[simp]
theorem Multiset.sort_sorted {α : Type u_1} (r : ααProp) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] (s : Multiset α) :
@[simp]
theorem Multiset.sort_eq {α : Type u_1} (r : ααProp) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] (s : Multiset α) :
↑(Multiset.sort r s) = s
@[simp]
theorem Multiset.mem_sort {α : Type u_1} (r : ααProp) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] {s : Multiset α} {a : α} :
@[simp]
theorem Multiset.length_sort {α : Type u_1} (r : ααProp) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] {s : Multiset α} :
List.length (Multiset.sort r s) = Multiset.card s
@[simp]
theorem Multiset.sort_zero {α : Type u_1} (r : ααProp) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] :
@[simp]
theorem Multiset.sort_singleton {α : Type u_1} (r : ααProp) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] (a : α) :
Multiset.sort r {a} = [a]
unsafe instance Multiset.instReprMultiset {α : Type u_1} [inst : Repr α] :
Equations
  • One or more equations did not get rendered due to their size.