zipWith — Mathlib

Lean4
/-- Given finitely supported functions `g₁ : α →₀ M` and `g₂ : α →₀ N` and function `f : M → N → P`,
`Finsupp.zipWith f hf g₁ g₂` is the finitely supported function `α →₀ P` satisfying
`zipWith f hf g₁ g₂ a = f (g₁ a) (g₂ a)`, which is well-defined when `f 0 0 = 0`. -/
def zipWith (f : M → N → P) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α →₀ N) : α →₀ P :=
  onFinset
    (haveI := Classical.decEq α;
    g₁.support ∪ g₂.support)
    (fun a => f (g₁ a) (g₂ a)) fun a (H : f _ _ ≠ 0) => by
    classical
    rw [mem_union, mem_support_iff, mem_support_iff, ← not_and_or]
    rintro ⟨h₁, h₂⟩; rw [h₁, h₂] at H; exact H hf
Похожие утверждения