zipRight_nil_cons — Mathlib

English

If the left list is empty and the right list is of the form b :: bs, then zipRight([], b :: bs) equals (None, b) :: map (b ↦ (None, b)) bs.

Русский

Если левый список пуст, а правый имеет вид b :: bs, то zipRight([], b :: bs) равно (None, b) :: map (λ b, (None, b)) bs.

LaTeX

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

Lean4

@[simp]
theorem zipRight_nil_cons : zipRight ([] : List α) (b :: bs) = (none, b) :: bs.map fun b => (none, b) :=
  rfl

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