eq_cons_iff — Mathlib

English

A vector is equal to a cons of a head and a tail iff its head equals a and its tail equals the tail vector.

Русский

Вектор равен конc-у головки и хвоста тогда и только тогда, когда голова равна заданному элементу, а хвост равен соответствующему вектору.

LaTeX

$$$\\forall {a} {v} {v'}:\\, v = a \\;::\\!ᵥ\\; v' \\iff v.head = a \\land v.tail = v'$$$

Lean4

theorem eq_cons_iff (a : α) (v : Vector α n.succ) (v' : Vector α n) : v = a ::ᵥ v' ↔ v.head = a ∧ v.tail = v' :=
  ⟨fun h => h.symm ▸ ⟨head_cons a v', tail_cons a v'⟩, fun h => _root_.trans (cons_head_tail v).symm (by rw [h.1, h.2])⟩

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