sort_nodup — Mathlib

English

Let s be a finite subset of a type equipped with a total order r. The list obtained by sorting s with respect to r contains every element of s exactly once; in particular it has no duplicates.

Русский

Пусть s — конечное подмножество типа, на котором задан полный порядок r. Отсортированный по r список элементов s содержит каждый элемент s ровно по одному разу; повторяющихся элементов нет.

LaTeX

$$$ \\operatorname{Nodup}(\\operatorname{sort}_r(s)) $$$

Lean4

@[simp]
theorem sort_nodup (s : Finset α) : (sort r s).Nodup :=
  (by rw [sort_eq]; exact s.2 : @Multiset.Nodup α (sort r s))

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