sortedUniv_nodup — Mathlib

English

Let α be a finite type equipped with an encoding. The list of all elements of α, taken in sorted order, contains no duplicates.

Русский

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

LaTeX

$$$\operatorname{Nodup}(\operatorname{sortedUniv} \alpha)$$$

Lean4

@[simp]
theorem sortedUniv_nodup (α) [Fintype α] [Encodable α] : (sortedUniv α).Nodup :=
  Finset.sort_nodup _ _

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