mem_or_mem_of_zipWith_swap_prod_ne

English

If (zipWith swap l l').prod x ≠ x, then x must occur in either l or l'.

Русский

Если (zipWith swap l l').prod x ≠ x, тогда x встречается в l или в l'.

LaTeX

$$$\\big((zipWith\\ swap\\ l\\ l').prod\\ x \\neq x\\big) \\Rightarrow (x \\in l \\lor x \\in l').$$$

Lean4

theorem mem_or_mem_of_zipWith_swap_prod_ne : ∀ {l l' : List α} {x : α}, (zipWith swap l l').prod x ≠ x → x ∈ l ∨ x ∈ l'
  | [], _, _ => by simp
  | _, [], _ => by simp
  | a :: l, b :: l', x => fun hx ↦
    if h : (zipWith swap l l').prod x = x then
      (eq_or_eq_of_swap_apply_ne_self (a := a) (b := b) (x := x) (by simpa [h] using hx)).imp
        (by rintro rfl; exact .head _) (by rintro rfl; exact .head _)
    else (mem_or_mem_of_zipWith_swap_prod_ne h).imp (.tail _) (.tail _)

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