sort — Mathlib

English

The operation sort r constructs a sorted list from a finite set s with respect to a total order r.

Русский

Операция sort r строит отсортированный список элементов конечного множества s по отношению порядка r.

LaTeX

$$$ \text{sort } r\ :\ \text{Finset } α \to \text{List } α $$$

Lean4

/-- `sort s` constructs a sorted list from the unordered set `s`.
  (Uses merge sort algorithm.) -/
def sort (s : Finset α) : List α :=
  Multiset.sort r s.1

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