nth_zero — Mathlib

English

Let Γ be a nonempty type and L be a ListBlank over Γ. Then the 0-th element of L equals its head: L.nth(0) = L.head.

Русский

Пусть Γ — непустой тип, а L — ListBlank над Γ. Тогда нулевой элемент L равен его голове: L.nth(0) = L.head.

LaTeX

$$$\forall {\Gamma} [Inhabited(\Gamma)]\,(l : ListBlank(\Gamma)),\ l.nth(0) = l.head$$$

Lean4

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

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