zipWith3_same_right — Mathlib

English

ZipWith3 f la lb lb equals zipWith (λ a b, f a b b) la lb.

Русский

ZipWith3 f la lb lb равно zipWith (λ a b, f a b b) la lb.

LaTeX

$$$zipWith3 f la lb lb = zipWith (\\lambda a b, f a b b) la lb$$$

Lean4

@[simp]
theorem zipWith3_same_right (f : α → β → β → γ) :
    ∀ (la : List α) (lb : List β), zipWith3 f la lb lb = zipWith (fun a b => f a b b) la lb
  | [], _ => rfl
  | _ :: _, [] => rfl
  | _ :: as, _ :: bs => congr_arg (cons _) <| zipWith3_same_right f as bs

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