zipRight'_nil_cons — Mathlib

English

For any bs, zipRight' ([] : List α) (b :: bs) = ((None, b) :: bs.map (λ b', (None, b')), [])

Русский

Для любого bs, zipRight' ([] : List α) (b :: bs) = ((None, b) :: bs.map (λ b', (None, b')), [])

LaTeX

$$$\\forall bs:\\text{List }\\beta,\\ \\mathrm{zipRight}'\\ (\\emptyset)\\ (b::bs) = ((\\mathrm{None}, b) :: bs.map(\\lambda b'. (\\mathrm{None}, b')), \\mathrm{[]})$$$

Lean4

@[simp]
theorem zipRight'_nil_cons : zipRight' ([] : List α) (b :: bs) = ((none, b) :: bs.map fun b => (none, b), []) :=
  rfl

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