nodup — Mathlib

English

A list sorted with an irreflexive relation implies nodupness.

Русский

Список, отсортированный по иррефлексивному отношению, имеет не повторяющиеся элементы.

LaTeX

$$$\\forall l:\\text{List}(\\alpha),\\; \\text{Sorted } r\\ l \\Rightarrow \\text{Nodup } l$$$

Lean4

protected theorem nodup {r : α → α → Prop} [IsIrrefl α r] {l : List α} (h : Sorted r l) : Nodup l :=
  Pairwise.nodup h

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