zipLeft'_cons_nil — Mathlib

English

For any a and as, zipLeft' (a :: as) ([]: List β) = ((a, None) :: as.map (a' ↦ (a', None)), []).

Русский

Для любого a и as, zipLeft' (a :: as) ([]: List β) = ((a, None) :: as.map (a' ↦ (a', None)), []).

LaTeX

$$$\\forall a:\\alpha,\\ \\forall as:\\text{List }\\alpha,\\ \\mathrm{zipLeft}'\\ (a::as)\\ ([]:\\text{List }\\beta) = ((a, \\mathrm{None}) :: as.map(\\\\lambda a'. (a', \\\\mathrm{None})), \\mathrm{[]})$$$

Lean4

@[simp]
theorem zipLeft'_cons_nil : zipLeft' (a :: as) ([] : List β) = ((a, none) :: as.map fun a => (a, none), []) :=
  rfl

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