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.)
Instances For
@[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]