get_inj_iff — Mathlib

English

If l is nodup, then for any i,j in Fin l.length, l.get i = l.get j iff i = j.

Русский

Если l нодуп, то для любых i,j из Fin(l.length) выполняется, что l.get i = l.get j тогда и только если i = j.

LaTeX

$$$ \forall i,j : Fin(l.length),\ l.get i = l.get j \iff i = j $$$

Lean4

theorem get_inj_iff {l : List α} (h : Nodup l) {i j : Fin l.length} : l.get i = l.get j ↔ i = j :=
  (nodup_iff_injective_get.1 h).eq_iff

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