zipWith_single_single — Mathlib

English

For any f and hf, zipWith f hf (single a m) (single a n) = single a (f m n).

Русский

Для любого f и hf, zipWith f hf (single a m) (single a n) = single a (f m n).

LaTeX

$$zipWith f hf (single a m) (single a n) = single a (f m n)$$

Lean4

@[simp]
theorem zipWith_single_single (f : M → N → P) (hf : f 0 0 = 0) (a : α) (m : M) (n : N) :
    zipWith f hf (single a m) (single a n) = single a (f m n) :=
  by
  ext a'
  rw [zipWith_apply]
  obtain rfl | ha' := eq_or_ne a' a
  · rw [single_eq_same, single_eq_same, single_eq_same]
  · rw [single_eq_of_ne ha', single_eq_of_ne ha', single_eq_of_ne ha', hf]

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