zipWith_congr — Mathlib

English

If f and g are pointwise equal on corresponding arguments with a pairwise equality, then zipWith f la lb = zipWith g la lb.

Русский

Если для всех соответствующих элементов la и lb верно f a b = g a b, то zipWith f la lb = zipWith g la lb.

LaTeX

$$$\forall f\, g\, la\, lb,\ Forall₂ (\\lambda a b, a b) la lb \to zipWith f la lb = zipWith g la lb$$$

Lean4

@[congr]
theorem zipWith_congr (f g : α → β → γ) (la : List α) (lb : List β)
    (h : List.Forall₂ (fun a b => f a b = g a b) la lb) : zipWith f la lb = zipWith g la lb := by
  induction h with
  | nil => rfl
  | cons hfg _ ih => exact congr_arg₂ _ hfg ih

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