finRange_eq_pmap_range

Mathlib.Data.List.FinRange

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

English

The list finRange(n) equals the pmap of Fin.mk on the range n.

Русский

Список finRange(n) равен отображению pmap от Fin.mk на диапазоне range n.

LaTeX

$$$\text{finRange}(n) = (\text{range}(n)).pmap (\text{Fin.mk}) (by\ simp)$$$

Lean4

theorem finRange_eq_pmap_range (n : ℕ) : finRange n = (range n).pmap Fin.mk (by simp) := by
  apply List.ext_getElem <;> simp [finRange]

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

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

Разделы

Аффилиация

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