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

• Multiset.sort r s = Quot.liftOn s (List.mergeSort r) (_ : ∀ (x x_1 : List α), Setoid.r x x_1 → List.mergeSort r x = List.mergeSort r x_1)

@[simp]

theorem Multiset.coe_sort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (l : List α) : Multiset.sort r ↑l = List.mergeSort r l

@[simp]

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

@[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 : α} : a ∈ Multiset.sort r s ↔ a ∈ s

@[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] : Multiset.sort r 0 = []

@[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 α] : Repr (Multiset α)

Equations

• One or more equations did not get rendered due to their size.