English
For any Γ with an element, and for all T: Tape Γ and any integer i, the nth symbol of T.write b equals b when i = 0, and equals T.nth i otherwise. Symbolically: (T.write b).nth i = if i = 0 then b else T.nth i.
Русский
Для любого Γ с элементом и любого T: Tape Γ и целого i, символ в позиции i после операции записи b равен b, если i = 0, иначе равен T.nth i.
LaTeX
$$$ \forall {\Gamma} [\text{Inhabited } {\Gamma}]\ (b: \Gamma)\ (T: \text{Tape } \Gamma)\ {i: \mathbb{Z}},\ (T.write b).nth i = \text{ite }(i = 0)\ b\ (T.nth i) $$$
Lean4
@[simp]
theorem write_nth {Γ} [Inhabited Γ] (b : Γ) : ∀ (T : Tape Γ) {i : ℤ}, (T.write b).nth i = if i = 0 then b else T.nth i
| _, 0 => rfl
| _, (_ + 1 : ℕ) => rfl
| _, -(_ + 1 : ℕ) => rfl
