map₂_cons — Mathlib

English

Mapping with map₂ on cons constructs preserves the head and recurses on the tail.

Русский

Применение map₂ к консу сохраняет голова и рекурсивно обрабатывает хвост.

LaTeX

$$$\forall\, hd_1\; tl_1\; hd_2\; tl_2\; f:\alpha\to\beta\to\gamma,\;\mathrm{Vector}.map_2\ f (hd_1::ᵥ tl_1) (hd_2::ᵥ tl_2) = f\ hd_1\ hd_2 ::ᵥ \mathrm{Vector}.map_2\ f tl_1 tl_2$$$

Lean4

@[simp]
theorem map₂_cons (hd₁ : α) (tl₁ : Vector α n) (hd₂ : β) (tl₂ : Vector β n) (f : α → β → γ) :
    Vector.map₂ f (hd₁ ::ᵥ tl₁) (hd₂ ::ᵥ tl₂) = f hd₁ hd₂ ::ᵥ (Vector.map₂ f tl₁ tl₂) :=
  rfl

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