zipWith_zipWith_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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