not_nodup_of_get_eq_of_ne — Mathlib

English

If xs has two different positions n and m with equal elements xs.get n = xs.get m, then xs is not nodup.

Русский

Если в списке xs существуют разные позиции n и m такие, что xs.get n = xs.get m, то xs содержит повторение.

LaTeX

$$$ \forall (xs: List\,\alpha)\ (n,m : Fin\,xs.length), xs.get n = xs.get m \rightarrow n \neq m \rightarrow \neg Nodup(xs) $$$

Lean4

theorem not_nodup_of_get_eq_of_ne (xs : List α) (n m : Fin xs.length) (h : xs.get n = xs.get m) (hne : n ≠ m) :
    ¬Nodup xs := by
  rw [nodup_iff_injective_get]
  exact fun hinj => hne (hinj h)

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