zipLeft'_nil_right — Mathlib

English

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

Русский

Для любых as и bs, zipLeft' f as ([]: List β) = (as.map (a ↦ (a, None)), []).

LaTeX

$$$\\forall f:\\alpha \\to \\mathrm{Option}\\,\\alpha \\to \\gamma\\ ,\\ \\mathrm{zipLeft}'\\ f\\ as\\ [] = (\\mathrm{as.map}(\\lambda a. (a, \\mathrm{None})), \\mathrm{[]})$$$

Lean4

@[simp]
theorem zipLeft'_nil_right : zipLeft' as ([] : List β) = (as.map fun a => (a, none), []) := by cases as <;> rfl

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