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
- 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)
[inst : DecidableRel r]
[inst : IsTrans α r]
[inst : IsAntisymm α r]
[inst : IsTotal α r]
(l : List α)
:
Multiset.sort r ↑l = List.mergeSort r l
@[simp]
theorem
Multiset.sort_sorted
{α : Type u_1}
(r : α → α → Prop)
[inst : DecidableRel r]
[inst : IsTrans α r]
[inst : IsAntisymm α r]
[inst : IsTotal α r]
(s : Multiset α)
:
List.Sorted r (Multiset.sort r s)
@[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 : α}
:
a ∈ Multiset.sort r s ↔ a ∈ s
@[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]
:
Multiset.sort r 0 = []
@[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]