nodup_mergeSort — Mathlib

English

The merge sort of a list is nodup exactly when the original list is nodup.

Русский

Объединённая сортировка списка имеет свойство нодуп тогда и только тогда, когда исходный список нодуп.

LaTeX

$$$ (\operatorname{l}.mergeSort(le)).Nodup \leftrightarrow \operatorname{l}.Nodup $$$

Lean4

@[simp]
theorem nodup_mergeSort {l : List α} {le : α → α → Bool} : (l.mergeSort le).Nodup ↔ l.Nodup :=
  (mergeSort_perm l le).nodup_iff

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