zipLeft'_cons_cons — Mathlib

English

For any a, as, b, bs, zipLeft' (a :: as) (b :: bs) equals let r := zipLeft' as bs in ((a, Some b) :: r.fst, r.snd).

Русский

Для любых a, as, b, bs: zipLeft'(a :: as) (b :: bs) = let r := zipLeft' as bs в ((a, Some b) :: r.fst, r.snd).

LaTeX

$$$\\forall a:\\alpha,\\ \\forall as:\\text{List }\\alpha,\\ \\forall b:\\beta,\\ \\forall bs:\\text{List }\\beta,\\ \\mathrm{zipLeft}'\\ (a::as)\\ (b::bs) =\\ let\\ r:=\\mathrm{zipLeft}'\\ as\\ bs\\ in\\ ((a, \\mathrm{Some}\\ b) :: r.fst, r.snd)$$$

Lean4

@[simp]
theorem zipLeft'_cons_cons :
    zipLeft' (a :: as) (b :: bs) =
      let r := zipLeft' as bs
      ((a, some b) :: r.fst, r.snd) :=
  rfl

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