Construct a sorted list from a multiset.

def Multiset.sort {α : Type u_1} (s : Multiset α) (r : α → α → Prop := by exact fun a b => a ≤ b) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] : List α

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

Equations

• s.sort r = Quot.liftOn s (fun (x : List α) => x.mergeSort fun (x1 x2 : α) => decide (r x1 x2)) ⋯

@[simp]

theorem Multiset.coe_sort {α : Type u_1} (l : List α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] : (↑l).sort r = l.mergeSort fun (x1 x2 : α) => decide (r x1 x2)

@[simp]

theorem Multiset.pairwise_sort {α : Type u_1} (s : Multiset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] : List.Pairwise r (s.sort r)

@[simp]

theorem Multiset.sort_eq {α : Type u_1} (s : Multiset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] : ↑(s.sort r) = s

@[simp]

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

@[simp]

theorem Multiset.sort_singleton {α : Type u_1} (a : α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] : {a}.sort r = [a]

theorem Multiset.map_sort {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] (r' : β → β → Prop) [DecidableRel r'] [IsTrans β r'] [Std.Antisymm r'] [Std.Total r'] (hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → (r a b ↔ r' (f a) (f b))) : List.map f (s.sort r) = (map f s).sort r'

theorem Multiset.sort_cons {α : Type u_1} (a : α) (s : Multiset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] : (∀ (b : α), b ∈ s → r a b) → (a ::ₘ s).sort r = a :: s.sort r

@[simp]

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

@[simp]

theorem Multiset.mem_sort {α : Type u_1} {a : α} {s : Multiset α} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] : a ∈ s.sort r ↔ a ∈ s

@[simp]

theorem Multiset.length_sort {α : Type u_1} {s : Multiset α} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] : (s.sort r).length = s.card

@[instance_reducible]

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

@[instance_reducible]

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

Equations

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