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 (fun (x : List α) => x.mergeSort fun (x1 x2 : α) => decide (r x1 x2)) ⋯
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 = l.mergeSort fun (x1 x2 : α) => decide (r x1 x2)
@[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 α}
:
(Multiset.sort r s).length = 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]
theorem
Multiset.map_sort
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
(r' : β → β → Prop)
[DecidableRel r']
[IsTrans β r']
[IsAntisymm β r']
[IsTotal β r']
(f : α → β)
(s : Multiset α)
(hs : ∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b))
:
List.map f (Multiset.sort r s) = Multiset.sort r' (Multiset.map f s)
theorem
Multiset.sort_cons
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
(a : α)
(s : Multiset α)
:
(∀ b ∈ s, r a b) → Multiset.sort r (a ::ₘ s) = a :: Multiset.sort r s