English
Let r be a relation on α. If r is biunique, then for any two lists l1 and l2 related componentwise by r (i.e., Forall₂ r l1 l2), l1 has no duplicates if and only if l2 has no duplicates.
Русский
Пусть r — отношение на α. Если r биоднозначно, то для любых списков l1 и l2, связанных компонентно отношением r (Forall₂ r l1 l2), у l1 нет повторяющихся элементов тогда и только тогда, когда у l2 тоже нет повторяющихся элементов.
LaTeX
$$$ \forall l_1 l_2,\ \operatorname{Forall}_2 r\; l_1\; l_2 \rightarrow ( \operatorname{Nodup}(l_1) \leftrightarrow \operatorname{Nodup}(l_2) ). $$$
Lean4
protected theorem nodup {l : List α} {r : α → α → Prop} [IsIrrefl α r] (h : Pairwise r l) : Nodup l :=
h.imp ne_of_irrefl
