mk'_nth_nat — Mathlib

English

If L and R are ListBlank Γ, then (Tape.mk' L R).nth n equals R.nth n (as a natural index cast).

Русский

Если L и R — ListBlank Γ, то (Tape.mk' L R).nth n равен R.nth n (для натурального n).

LaTeX

$$$\forall {\Gamma} [Inhabited(\Gamma)] (L R : ListBlank(\Gamma)) (n : \mathbb{N}), (Tape.mk' L R).nth n = R.nth n$$$

Lean4

@[simp]
theorem mk'_nth_nat {Γ} [Inhabited Γ] (L R : ListBlank Γ) (n : ℕ) : (Tape.mk' L R).nth n = R.nth n := by
  rw [← Tape.right₀_nth, Tape.mk'_right₀]

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