map₂_snoc

Mathlib.Data.Vector.Snoc

URI: https://scilib.ai/kg/mathlib#List.Vector.map₂_snoc

← MathLib Explorer

English

map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y).

Русский

map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y).

LaTeX

$$$\text{map₂ } f (xs.snoc x) (ys.snoc y) = (\text{map₂ } f xs ys).snoc (f x y)$$$

Lean4

@[simp]
theorem map₂_snoc {f : α → β → σ} {y : β} : map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y) := by
  induction xs, ys using Vector.inductionOn₂ <;> simp_all

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

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

Разделы

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

Аффилиация

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