zipRight_cons_cons — Mathlib

English

If both lists are nonempty, with left head a and tail as, and right head b and tail bs, then zipRight(a :: as, b :: bs) = (Some a, b) :: zipRight as bs.

Русский

Если обе списки ненулевые: слева голова a и хвост as, справа голова b и хвост bs, тогда zipRight(a :: as, b :: bs) = (Some a, b) :: zipRight as bs.

LaTeX

$$$ \operatorname{zipRight}(a :: as, b :: bs) = (\mathrm{Some}\, a, b) :: \operatorname{zipRight}(as, bs)$$$

Lean4

@[simp]
theorem zipRight_cons_cons : zipRight (a :: as) (b :: bs) = (some a, b) :: zipRight as bs :=
  rfl

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