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)) ⋯

@[simp]

theorem Multiset.coe_sort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (l : List α) : 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 (sort r s)

@[simp]

theorem Multiset.sort_eq {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (s : 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 ∈ 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 α} : (sort r s).length = s.card

@[simp]

theorem Multiset.sort_zero {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : sort r 0 = []

@[simp]

theorem Multiset.sort_singleton {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (a : α) : 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 (sort r s) = sort r' (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) → sort r (a ::ₘ s) = a :: sort r s

@[simp]

theorem Multiset.sort_range (n : ℕ) : sort (fun (x1 x2 : ℕ) => x1 ≤ x2) (range n) = List.range n

unsafe instance Multiset.instToExprOfToLevel {α : Type u} [Lean.ToLevel] [Lean.ToExpr α] : Lean.ToExpr (Multiset α)

unsafe instance Multiset.instRepr {α : Type u_1} [Repr α] : Repr (Multiset α)

Equations

• One or more equations did not get rendered due to their size.