cons_head_tail — Mathlib

English

For every ListBlank l, the operation tail followed by cons with head recovers the original list: tail l and head l are inverse.

Русский

Для любого ListBlank l операция tail l затем добавление head l восстанавливает исходный список: head и tail взаимно обратны.

LaTeX

$$$\\forall l:\\text{ListBlank }\\Gamma,\\ (l.tail).cons(l.head) = l$$$

Lean4

/-- The `cons` and `head`/`tail` functions are mutually inverse, unlike in the case of `List` where
this only holds for nonempty lists. -/
@[simp]
theorem cons_head_tail {Γ} [Inhabited Γ] : ∀ l : ListBlank Γ, l.tail.cons l.head = l :=
  by
  apply Quotient.ind'
  refine fun l ↦ Quotient.sound' (Or.inr ?_)
  cases l
  · exact ⟨1, rfl⟩
  · rfl

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