map₂Right'_nil_cons — Mathlib

English

For any f : α → Option β → γ and any bs, map₂Right' f [] (b :: bs) = (f none b :: bs.map (f none), []).

Русский

Для любого f : α → Option β → γ и списка bs, map₂Right' f [] (b :: bs) = (f none b :: bs.map (f none), []).

LaTeX

$$$\\forall f:\\alpha \\to \\mathrm{Option}\\,\\beta \\to \\gamma\\ ,\\ \\mathrm{map₂Right}'\\ f\\ \\emptyset\\ (b::bs) = (f\\ none\\ b :: bs.map(\\lambda b'. f\\ none\\ b'),\\ emptyset)$$$

Lean4

@[simp]
theorem map₂Right'_nil_cons : map₂Right' f [] (b :: bs) = (f none b :: bs.map (f none), []) :=
  rfl

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