zipRight_nil_left — Mathlib

English

Let bs be a list of elements of β. Then zipRight([], bs) equals the list formed by pairing None with each element of bs.

Русский

Пусть bs — список элементов β. Тогда zipRight([], bs) равен списку, получаемому сопоставлениемNone каждому элементу bs.

LaTeX

$$$ \operatorname{zipRight}(\varnothing, bs) = \operatorname{map}(b \mapsto (\mathrm{None}, b))\, bs$$$

Lean4

@[simp]
theorem zipRight_nil_left : zipRight ([] : List α) bs = bs.map fun b => (none, b) := by cases bs <;> rfl

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