get?_zipWith — Mathlib

English

For any function f, sequences s and s', and index n, the nth element of zipWith f s s' is obtained by applying f to the nth elements of s and s' when both are defined.

Русский

Для любой функции f и последовательностей s и s' и индекса n, n-й элемент zipWith f s s' получается применением f к n-й элементам s и s' при условии, что оба существуют.

LaTeX

$$$$ \\mathrm{get?}(\\mathrm{zipWith}\\ f\\ s\\ s')\\ n = \\mathrm{map}_2\\ f\\bigl(\\mathrm{get?}\\ s\\ n\\bigr)\\bigl(\\mathrm{get?}\\ s'\\ n\\bigr). $$$$

Lean4

@[simp]
theorem get?_zipWith (f : α → β → γ) (s s' n) : (zipWith f s s').get? n = Option.map₂ f (s.get? n) (s'.get? n) :=
  rfl

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