sort_sorted — Mathlib

English

The sorted order of a multiset is a canonical representative of the multiset under the given total order.

Русский

Упорядоченный сортированный порядок мультиcета является каноническим представителем мультисета по данному полному порядку.

LaTeX

$$$$ \\uparrow(\\operatorname{sort} r s) = s $$$$

Lean4

@[simp]
theorem sort_sorted (s : Multiset α) : Sorted r (sort r s) :=
  Quot.inductionOn s (sorted_mergeSort' _)

Похожие утверждения