set

Mathlib.Data.Vector.Basic

URI: https://scilib.ai/kg/mathlib#List.Vector.set

← MathLib Explorer

English

Set v i a replaces the i-th element of v by a, leaving the rest unchanged.

Русский

Заменяет i-й элемент вектора v на a, остальные элементы не меняются.

LaTeX

$$$\\text{set} (v)\\; (i)\\; (a) : \\ Vector\\ α\\ n$$$

Lean4

/-- `set v n a` replaces the `n`th element of `v` with `a`. -/
def set (v : Vector α n) (i : Fin n) (a : α) : Vector α n :=
  ⟨v.1.set i.1 a, by simp⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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