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})))$$$

Lean4

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

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