idxOf_finRange

Mathlib.Data.List.FinRange

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

English

If k is a natural number and i : Fin k, then the position of i in the FinRange k equals i: (finRange k).idxOf i = i.

Русский

Пусть k ∈ ℕ и i : Fin k. Позиция i в списке FinRange k равна i: (finRange k).idxOf i = i.

LaTeX

$$$$ (finRange\\ k).idxOf i = i. $$$$

Lean4

@[simp]
theorem idxOf_finRange {k : ℕ} (i : Fin k) : (finRange k).idxOf i = i := by
  simpa using idxOf_getElem (nodup_finRange k) i

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

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

Разделы

Аффилиация

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