English
For any f : α → Option β → γ and any list as, the left-mapped pair with an empty right list is computed componentwise: map₂Left' f as [] = (as.map (a ↦ f a none), []).\n
Русский
Для любой f : α → Option β → γ и списка as правая часть пустого списка не учитывается; левая часть задаётся поэлементно: map₂Left' f as [] = (as.map (a ↦ f a none), []).
LaTeX
$$$\\forall f:\\alpha \\to \\mathrm{Option}\\,\\beta \\to \\gamma\\ ,\\ \\mathrm{map₂Left}'\\ f\\ as\\ [] = \\left(\\mathrm{as.map}(\\lambda a. f\\ a\\ \\mathrm{none}),\\ \\mathrm{[]}\\right)$$$
Lean4
@[simp]
theorem map₂Left'_nil_right (f : α → Option β → γ) (as) : map₂Left' f as [] = (as.map fun a => f a none, []) := by
cases as <;> rfl
