mathlib documentation

data.multiset.sort

Construct a sorted list from a multiset.

def multiset.sort {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] :
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) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] (l : list α) :

@[simp]
theorem multiset.sort_sorted {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] (s : multiset α) :

@[simp]
theorem multiset.sort_eq {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] (s : multiset α) :

@[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 : α} :

@[simp]
theorem multiset.length_sort {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] {s : multiset α} :

@[instance]
def multiset.has_repr {α : Type u_1} [has_repr α] :

Equations