ne_cons_iff — Mathlib

English

A vector is not equal to a cons of head and tail iff either the head differs or the tail differs.

Русский

Вектор не равен конc-у головки и хвоста тогда и только тогда, когда головы не равны или хвосты не равны.

LaTeX

$$$v \\neq a \\\\!::\\\\!ᵥ v' \\iff v.head \\neq a \\\\lor v.tail \\neq v'$$$

Lean4

theorem ne_cons_iff (a : α) (v : Vector α n.succ) (v' : Vector α n) : v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v' := by
  rw [Ne, eq_cons_iff a v v', not_and_or]

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