English
If r is a biunique relation on α, then for any two lists l1 and l2 related componentwise by r, the two lists have the same nodup status (both nodup or both not nodup).
Русский
Если r — биуникальное отношение на α, то для любых списков l1 и l2, связанных по компонентам отношением r, их свойство отсутствия повторов совпадает: либо оба списки без повторов, либо оба содержат повторения.
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
theorem rel_nodup {r : α → β → Prop} (hr : Relator.BiUnique r) : (Forall₂ r ⇒ (· ↔ ·)) Nodup Nodup
| _, _, Forall₂.nil => by simp only [nodup_nil]
| _, _, Forall₂.cons hab h => by
simpa only [nodup_cons] using Relator.rel_and (Relator.rel_not (rel_mem hr hab h)) (rel_nodup hr h)
