English
zipWith f takes two vectors of the same length and returns a vector by applying f pointwise to corresponding elements.
Русский
zipWith f берет два вектора одинаковой длины и возвращает вектор, полученный применением f по точкам к соответствующим элементам.
LaTeX
$$$\text{zipWith} : Vector\ α\ n \to Vector\ β\ n \to Vector\ γ\ n$ with $\text{zipWith } f\ x\ y = \langle\text{List.zipWith } f\ x.1\ y.1, \ \dots \rangle$$$
Lean4
/-- Apply the function `f : α → β → γ` to each corresponding pair of elements from two vectors. -/
def zipWith : Vector α n → Vector β n → Vector γ n := fun x y => ⟨List.zipWith f x.1 y.1, by simp⟩
