nodup_iff_injective_getElem — Mathlib

English

A list l is nodup if and only if the function assigning to each index its element is injective.

Русский

Список l является нодуп тогда и только тогда, когда отображение индекса в элемент является инъективным.

LaTeX

$$$ \operatorname{Nodup}(l) \iff \operatorname{Injective}(l.get) $$$

Lean4

theorem nodup_iff_injective_getElem {l : List α} : Nodup l ↔ Function.Injective (fun i : Fin l.length => l[i.1]) :=
  pairwise_iff_getElem.trans
    ⟨fun h i j hg => by
      obtain ⟨i, hi⟩ := i; obtain ⟨j, hj⟩ := j
      rcases lt_trichotomy i j with (hij | rfl | hji)
      · exact (h i j hi hj hij hg).elim
      · rfl
      · exact (h j i hj hi hji hg.symm).elim, fun hinj i j hi hj hij h =>
      Nat.ne_of_lt hij (Fin.val_eq_of_eq (@hinj ⟨i, hi⟩ ⟨j, hj⟩ h))⟩

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