mathlib3 documentation

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) [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
@[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 α} :
@[simp]
theorem multiset.sort_zero {α : Type u_1} (r : α α Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] :
@[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]
@[protected, instance]
meta def multiset.has_repr {α : Type u_1} [has_repr α] :