Theorems · Definition · combinatorics

Multiset.sort

{α : Type u_1} →
  Multiset α →
    (r : autoParam (α → α → Prop) Multiset.sort._auto_1) →
      [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.)

Defined in

Mathlib.Data.Multiset.Sort

Cited by

19 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Quot.sound

Assumes

DecidableRelIsTransStd.AntisymmStd.Total