get?_zip — Mathlib

English

The nth element of the zipped sequence of s and t is the pair of their nth elements, when both exist.

Русский

n-й элемент зип-последовательности s и t является парой их n-й элементов, если оба существуют.

LaTeX

$$$$ \\text{get?}(\\mathrm{zip}\\ s\\ t)\\ n = \\mathrm{map}\\bigl( \\mathrm{Prod.mk} \\ n\\bigr)\\bigl( \\text{get?}(s,n) \\bigr) \\otimes \\bigl( \\text{get?}(t,n) \\bigr). $$$$

Lean4

@[simp]
theorem get?_zip (s : Seq α) (t : Seq β) (n : ℕ) : get? (zip s t) n = Option.map₂ Prod.mk (get? s n) (get? t n) :=
  get?_zipWith _ _ _ _

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