nth_succ — Mathlib

English

Let Γ be nonempty. For any ListBlank L and any natural n, the (n+1)-st element of L equals the nth element of its tail: L.nth(n+1) = L.tail.nth(n).

Русский

Пусть Γ ненулевая, для любого ListBlank L и любого натурального n, (n+1)-й элемент L равен n-му элементу хвоста: L.nth(n+1) = L.tail.nth(n).

LaTeX

$$$\forall {\Gamma} [Inhabited(\Gamma)]\,(l : ListBlank(\Gamma))\ (n : \mathbb{N}),\ l.nth(n+1) = l.tail.nth(n)$$$

Lean4

@[simp]
theorem nth_succ {Γ} [Inhabited Γ] (l : ListBlank Γ) (n : ℕ) : l.nth (n + 1) = l.tail.nth n :=
  by
  conv => lhs; rw [← ListBlank.cons_head_tail l]
  exact Quotient.inductionOn' l.tail fun l ↦ rfl

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