English
For maps f, g1, g2, the operation zipWith combines the two dependent products into a single DFinsupp with coordinates given by f i (g1 i) (g2 i).
Русский
Операция zipWith объединяет два зависимых произведения в единый DFinsupp, координаты заданы как f i (g1 i) (g2 i).
LaTeX
$$$\\mathrm{zipWith}\,f\,hf\,g_1\,g_2 = \\mathrm{mk}(g_1.{\\mathrm{support}} \\cup g_2.{\\mathrm{support}})\\; (\\lambda i, f i.1 (g_1 i.1) (g_2 i.1))$$$
Lean4
theorem zipWith_def {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : DecidableEq ι]
[∀ i : ι, Zero (β i)] [∀ i : ι, Zero (β₁ i)] [∀ i : ι, Zero (β₂ i)] [∀ (i : ι) (x : β₁ i), Decidable (x ≠ 0)]
[∀ (i : ι) (x : β₂ i), Decidable (x ≠ 0)] {f : ∀ i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0} {g₁ : Π₀ i, β₁ i}
{g₂ : Π₀ i, β₂ i} : zipWith f hf g₁ g₂ = mk (g₁.support ∪ g₂.support) fun i => f i.1 (g₁ i.1) (g₂ i.1) :=
by
ext i
by_cases h1 : g₁ i ≠ 0 <;> by_cases h2 : g₂ i ≠ 0 <;> simp only [not_not, Ne] at h1 h2 <;> simp [h1, h2, hf]
