sort_sorted_lt — Mathlib

English

For a finite set in a linear order, the sorted list is strictly sorted with respect to < when using the natural ≤ order for sorting.

Русский

Для конечного множества в линейном порядке отсортованный список упорядочен строго по < при использовании естественного ≤ для сортировки.

LaTeX

$$$ \\text{List.Sorted}(<)\\,(\\operatorname{sort}_{\\le} s) $$$

Lean4

theorem sort_sorted_lt (s : Finset α) : List.Sorted (· < ·) (sort (· ≤ ·) s) :=
  (sort_sorted _ _).lt_of_le (sort_nodup _ _)

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