support_zipWith — Mathlib

English

The support of zipWith is contained in the union of the supports of the two operands.

Русский

Опора zipWith содержится в объединении опор двух операндов.

LaTeX

$$$\\operatorname{supp}(\\mathrm{zipWith}\\,f\\,hf\\,g_1\\,g_2) \\subseteq g_1.{\\mathrm{support}} \\cup g_2.{\\mathrm{support}}$$$

Lean4

theorem support_zipWith {f : ∀ i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0} {g₁ : Π₀ i, β₁ i} {g₂ : Π₀ i, β₂ i} :
    (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support := by simp [zipWith_def]

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