English
If f : M → N with hf : f 0 = 0 and g1,g2 are finsupps on α with values in M,N respectively, then the support of zipWith f hf g1 g2 is contained in the union of the supports of g1 and g2.
Русский
Пусть f : M → N с hf : f 0 = 0 и l1,l2 — функции с конечной опорой, соответствующие M и N. Тогда поддержка zipWith f hf l1 l2 ⊆ поддержка l1 ∪ поддержка l2.
LaTeX
$$$\\operatorname{support}(\\mathrm{zipWith} f hf\\ g_1\\ g_2) \\subseteq \\operatorname{support}(g_1) \\cup \\operatorname{support}(g_2)$$$
Lean4
theorem support_zipWith [D : DecidableEq α] {f : M → N → P} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} :
(zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support := by convert support_onFinset_subset
