zipLeft_cons_cons — Mathlib

English

For any a, as, b, bs, zipLeft (a :: as) (b :: bs) = ((a, Some b) :: as.zipLeft bs, bs).

Русский

Для любых a, as, b, bs: zipLeft (a :: as) (b :: bs) = ((a, Some b) :: as.zipLeft bs, bs).

LaTeX

$$$\\forall a:\\alpha,\\ \\forall as:\\text{List }\\alpha,\\ \\forall b:\\beta,\\ \\forall bs:\\text{List }\\beta,\\ \\mathrm{zipLeft} (a::as) (b::bs) = \\left( (a, \\mathrm{Some}\\ b) :: as.zipLeft bs, bs \\right)$$$

Lean4

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

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