right₀_nth — Mathlib

English

For any Tape T and natural n, T.right₀.nth n = T.nth n.

Русский

Для любой ленты T и натурального n, T.right₀.nth n = T.nth n.

LaTeX

$$$\forall {\Gamma} [Inhabited(\Gamma)] (T : Tape(\Gamma)) (n : \mathbb{N}), T.right_0.nth n = T.nth n$$$

Lean4

theorem right₀_nth {Γ} [Inhabited Γ] (T : Tape Γ) (n : ℕ) : T.right₀.nth n = T.nth n := by
  cases n <;>
    simp only [Tape.nth, Tape.right₀, ListBlank.nth_zero, ListBlank.nth_succ, ListBlank.head_cons, ListBlank.tail_cons]

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