Multiset.sort_eq

theorem Multiset.sort_eq : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : IsAntisymm α r] [inst_3 : IsTotal α r] (s : Multiset α), ↑(Multiset.sort r s) = s

This theorem asserts that for any given type `α`, relation `r` on `α` that is decidable, transitive, antisymmetric and total, and any multiset `s` of type `α`, the sorted list obtained from multiset `s` by using the `Multiset.sort` operation, when converted back to a multiset, is equivalent to the original multiset `s`. This essentially means that the sorting process doesn't alter the original collection of elements, it just rearranges them in an ordered manner.

More concisely: For any decidable, transitive, antisymmetric and total relation `r` on type `α` and multiset `s` of type `α`, `Multiset.sort r s` is equivalent to `s`.