English
Let f assign to each index i a bilinear map f i : β1 i → β2 i → β i, with hf : ∀ i, f i 0 0 = 0. Then for any index i and any b1 ∈ β1 i, b2 ∈ β2 i, the operation zipWith applied to the two singles at i satisfies zipWith f hf (single i b1) (single i b2) = single i (f i b1 b2).
Русский
Пусть f задаёт для каждого i билинейную билинную карту f i : β1 i → β2 i → β i, причём hf : ∀ i, f i 0 0 = 0. Тогда для любого индекса i и элементов b1 ∈ β1 i, b2 ∈ β2 i выполняется равенство zipWith f hf (single i b1) (single i b2) = single i (f i b1 b2).
LaTeX
$$$\\\\operatorname{zipWith} f hf \\\\ (\\\\mathrm{single} i b_{1}) \\\\ (\\\\mathrm{single} i b_{2}) = \\\\mathrm{single} i \\\\left( f i b_{1} b_{2} \\\\right). $$$
Lean4
@[simp]
theorem zipWith_single_single (f : ∀ i, β₁ i → β₂ i → β i) (hf : ∀ i, f i 0 0 = 0) {i} (b₁ : β₁ i) (b₂ : β₂ i) :
zipWith f hf (single i b₁) (single i b₂) = single i (f i b₁ b₂) :=
by
ext j
rw [zipWith_apply]
obtain rfl | hij := Decidable.eq_or_ne j i
· rw [single_eq_same, single_eq_same, single_eq_same]
· rw [single_eq_of_ne hij, single_eq_of_ne hij, single_eq_of_ne hij, hf]
