zipWith_zipWith_right — Mathlib

English

ZipWith f la (zipWith g lb lc) equals zipWith3 with a lambda: (a,b,c) ↦ f a (g b c).

Русский

ZipWith f la (zipWith g lb lc) равно zipWith3 с функцией: (a,b,c) ↦ f a (g b c).

LaTeX

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

Lean4

theorem zipWith_zipWith_right (f : α → δ → ε) (g : β → γ → δ) :
    ∀ (la : List α) (lb : List β) (lc : List γ),
      zipWith f la (zipWith g lb lc) = zipWith3 (fun a b c => f a (g b c)) la lb lc
  | [], _, _ => rfl
  | _ :: _, [], _ => rfl
  | _ :: _, _ :: _, [] => rfl
  | _ :: as, _ :: bs, _ :: cs => congr_arg (cons _) <| zipWith_zipWith_right f g as bs cs

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