zipWith3_same_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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