zipWith_swap_prod_support — Mathlib

English

For finite α, the support of (zipWith swap l l').prod is contained in l.toFinset ∪ l'.toFinset.

Русский

При конечном α, поддержка (zipWith swap l l').prod ⊆ l.toFinset ∪ l'.toFinset.

LaTeX

$$$(zipWith\\ swap\\ l\\ l').prod.status \\;\\mathrm{support} \\subseteq l^{\\mathrm{toFinset}} \\cup l'^{\\mathrm{toFinset}}$$$

Lean4

theorem zipWith_swap_prod_support [Fintype α] (l l' : List α) :
    (zipWith swap l l').prod.support ≤ l.toFinset ⊔ l'.toFinset :=
  by
  intro x hx
  have hx' : x ∈ {x | (zipWith swap l l').prod x ≠ x} := by simpa using hx
  simpa using zipWith_swap_prod_support' _ _ hx'

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