getD_replicate

Mathlib.Data.List.GetD

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

English

If i < n, then getD of the replicate list at i is equal to the replicated element.

Русский

Если i < n, то getD для списка replicate на позиции i равен скопированному элементу.

LaTeX

$$$$ i < n \\Rightarrow (\\mathrm{replicate}\\ n\\ x).getD i y = x $$$$

Lean4

theorem getD_replicate {y i n} (h : i < n) : getD (replicate n x) i y = x :=
  by
  rw [getD_eq_getElem, getElem_replicate]
  rwa [length_replicate]

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

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

Разделы

Аффилиация

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