English
A list l is nodup if and only if for all i,j, i<j, l[i]? ≠ l[j]?, where getElem? returns an optional element.
Русский
Список l нодуп тогда, когда для всех i, j, i<j, l[i]? ≠ l[j]?, где getElem? возвращает элемент в опции.
LaTeX
$$$ l.Nodup \iff \forall i j : \mathbb{N}, i < j \rightarrow j < l.length \rightarrow l[i]? \neq l[j]? $$$
Lean4
theorem nodup_iff_getElem?_ne_getElem? {l : List α} : l.Nodup ↔ ∀ i j : ℕ, i < j → j < l.length → l[i]? ≠ l[j]? :=
by
rw [Nodup, pairwise_iff_getElem]
constructor
· intro h i j hij hj
rw [getElem?_eq_getElem (lt_trans hij hj), getElem?_eq_getElem hj, Ne, Option.some_inj]
exact h _ _ (by cutsat) hj hij
· intro h i j hi hj hij
rw [Ne, ← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem]
exact h i j hij hj
