map_id

Mathlib.Data.Vector.Basic

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

← MathLib Explorer

English

Mapping by the identity function leaves a vector unchanged.

Русский

Отображение по единичной функции не меняет вектор.

LaTeX

$$$\forall v:\mathrm{Vector}\,\alpha\,n,\; \mathrm{Vector}.map\ id\ v = v$$$

Lean4

/-- Mapping under `id` does not change a vector. -/
@[simp]
theorem map_id {n : ℕ} (v : Vector α n) : Vector.map id v = v :=
  Vector.eq _ _ (by simp only [List.map_id, Vector.toList_map])

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

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

Разделы

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

Аффилиация

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