zipWith_tail

Mathlib.Data.Vector.Zip

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

← MathLib Explorer

English

The tail of Vector.zipWith f x y equals Vector.zipWith f x.tail y.tail.

Русский

Хвост Vector.zipWith f x y равен Vector.zipWith f x.tail y.tail.

LaTeX

$$$\text{Vector.zipWith } f x y\text{.tail} = \text{Vector.zipWith } f x.tail y.tail$$$

Lean4

@[simp]
theorem zipWith_tail (x : Vector α n) (y : Vector β n) : (Vector.zipWith f x y).tail = Vector.zipWith f x.tail y.tail :=
  by
  ext
  simp [get_tail]

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

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

Разделы

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

Аффилиация

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