map₂Right'_nil_left — Mathlib

English

For any f : α → Option α → γ and any bs, map₂Right' f [] bs = (bs.map (f none), []), i.e. the left side is empty and the right is carried over with f none.

Русский

Для любого f : α → Option α → γ и любого bs, map₂Right' f [] bs = (bs.map (f none), []) — левая часть пустая, правая передаётся через f none.

LaTeX

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

Lean4

@[simp]
theorem map₂Right'_nil_left : map₂Right' f [] bs = (bs.map (f none), []) := by cases bs <;> rfl

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