zipWith_swap_prod_support' — Mathlib

English

The moved points of the permutation zipWith swap l l' are contained in l ∪ l'.

Русский

Поддержка перемещения перестановки zipWith swap ∘ l l' ∘ движется только в пределах l ∪ l'.

LaTeX

$$$\\{x \\mid (zipWith\\ swap\\ l\\ l').prod\\ x \\neq x\\} \\subseteq l^{\\!\\text{toFinset}} \\sqcup l'^{\\!\\text{toFinset}}$$$

Lean4

theorem zipWith_swap_prod_support' (l l' : List α) : {x | (zipWith swap l l').prod x ≠ x} ≤ l.toFinset ⊔ l'.toFinset :=
  fun _ h ↦ by simpa using mem_or_mem_of_zipWith_swap_prod_ne h

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