get_idxOf

Mathlib.Data.List.Nodup

URI: https://scilib.ai/kg/mathlib#List.get_idxOf

English

If l is nodup, then for any i: Fin l.length, idxOf (get l i) l = i.

Русский

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

LaTeX

$$$ [DecidableEq \alpha] \Rightarrow \forall i : Fin\ l.length, \operatorname{idxOf}(l.get i, l) = i $$$

Lean4

theorem get_idxOf [DecidableEq α] {l : List α} (H : Nodup l) (i : Fin l.length) : idxOf (get l i) l = i := by
  simp [idxOf_getElem, H]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru