mem_succ_iff — Mathlib

English

If v has length n+1, then a ∈ v.toList iff a = head or a ∈ tail.toList.

Русский

Если длина вектора v равна n+1, то a ∈ v.toList тогда и только тогда, когда a = head или a ∈ tail.toList.

LaTeX

$$$$ a \in v.toList \iff a = v.head \lor a \in v.tail.toList $$$$

Lean4

theorem mem_succ_iff (v : Vector α (n + 1)) : a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList :=
  by
  obtain ⟨a', v', h⟩ := exists_eq_cons v
  simp_rw [h, Vector.mem_cons_iff, Vector.head_cons, Vector.tail_cons]

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