Construct a sorted list from a multiset. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
def
multiset.sort
{α : Type u_1}
(r : α → α → Prop)
[decidable_rel r]
[is_trans α r]
[is_antisymm α r]
[is_total α r]
(s : multiset α) :
list α
sort s constructs a sorted list from the multiset s.
(Uses merge sort algorithm.)
Equations
- multiset.sort r s = quot.lift_on s (list.merge_sort r) _
@[simp]
theorem
multiset.coe_sort
{α : Type u_1}
(r : α → α → Prop)
[decidable_rel r]
[is_trans α r]
[is_antisymm α r]
[is_total α r]
(l : list α) :
multiset.sort r ↑l = list.merge_sort r l
@[simp]
theorem
multiset.sort_sorted
{α : Type u_1}
(r : α → α → Prop)
[decidable_rel r]
[is_trans α r]
[is_antisymm α r]
[is_total α r]
(s : multiset α) :
list.sorted r (multiset.sort r s)
@[simp]
theorem
multiset.sort_eq
{α : Type u_1}
(r : α → α → Prop)
[decidable_rel r]
[is_trans α r]
[is_antisymm α r]
[is_total α r]
(s : multiset α) :
↑(multiset.sort r s) = s
@[simp]
theorem
multiset.mem_sort
{α : Type u_1}
(r : α → α → Prop)
[decidable_rel r]
[is_trans α r]
[is_antisymm α r]
[is_total α r]
{s : multiset α}
{a : α} :
a ∈ multiset.sort r s ↔ a ∈ s
@[simp]
theorem
multiset.length_sort
{α : Type u_1}
(r : α → α → Prop)
[decidable_rel r]
[is_trans α r]
[is_antisymm α r]
[is_total α r]
{s : multiset α} :
(multiset.sort r s).length = ⇑multiset.card s
@[simp]
theorem
multiset.sort_zero
{α : Type u_1}
(r : α → α → Prop)
[decidable_rel r]
[is_trans α r]
[is_antisymm α r]
[is_total α r] :
multiset.sort r 0 = list.nil
@[simp]
theorem
multiset.sort_singleton
{α : Type u_1}
(r : α → α → Prop)
[decidable_rel r]
[is_trans α r]
[is_antisymm α r]
[is_total α r]
(a : α) :
multiset.sort r {a} = [a]