getElem_inj_iff — Mathlib

English

If l is nodup, then for any i and j with hi,hj, l[i] = l[j] iff i = j.

Русский

Если l нодуп, тогда для любых i и j с hi, hj, l[i] = l[j] тогда и только если i = j.

LaTeX

$$$ l.Nodup \rightarrow \forall i,j \, (hi : i < l.length) (hj : j < l.length), \ l[i] = l[j] \iff i = j $$$

Lean4

theorem getElem_inj_iff {l : List α} (h : Nodup l) {i : Nat} {hi : i < l.length} {j : Nat} {hj : j < l.length} :
    l[i] = l[j] ↔ i = j := by
  have := @Nodup.get_inj_iff _ _ h ⟨i, hi⟩ ⟨j, hj⟩
  simpa

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