tail_map

Mathlib.Data.Vector.Basic

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

← MathLib Explorer

English

The tail after mapping equals the image of the tail under f.

Русский

Хвост после отображения равен образу хвоста: (v.map f).tail = v.tail.map f.

LaTeX

$$$(v.map f).tail = v.tail.map f$$$

Lean4

@[simp]
theorem tail_map {β : Type*} (v : Vector α (n + 1)) (f : α → β) : (v.map f).tail = v.tail.map f :=
  by
  obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
  rw [h, map_cons, tail_cons, tail_cons]

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

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

Разделы

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

Аффилиация

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