# mathlib3documentation

data.multiset.sort

# 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) [ r] [ r] [ r] (s : multiset α) :
list α

sort s constructs a sorted list from the multiset s. (Uses merge sort algorithm.)

Equations
• = _
@[simp]
theorem multiset.coe_sort {α : Type u_1} (r : α α Prop) [ r] [ r] [ r] (l : list α) :
=
@[simp]
theorem multiset.sort_sorted {α : Type u_1} (r : α α Prop) [ r] [ r] [ r] (s : multiset α) :
s)
@[simp]
theorem multiset.sort_eq {α : Type u_1} (r : α α Prop) [ r] [ r] [ r] (s : multiset α) :
s) = s
@[simp]
theorem multiset.mem_sort {α : Type u_1} (r : α α Prop) [ r] [ r] [ r] {s : multiset α} {a : α} :
a a s
@[simp]
theorem multiset.length_sort {α : Type u_1} (r : α α Prop) [ r] [ r] [ r] {s : multiset α} :
s).length =
@[simp]
theorem multiset.sort_zero {α : Type u_1} (r : α α Prop) [ r] [ r] [ r] :
@[simp]
theorem multiset.sort_singleton {α : Type u_1} (r : α α Prop) [ r] [ r] [ r] (a : α) :
{a} = [a]
@[protected, instance]
meta def multiset.has_repr {α : Type u_1} [has_repr α] :