zipWith3_same_mid — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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