English
Mapping a tape after Mk' is the same as Mk' of the mapped left and right lists.
Русский
Отображение на ленте после Mk' эквивалентно Mk' отображения левых и правых списков.
LaTeX
$$$ \forall {\Gamma} {\Gamma'} [\text{Inhabited } {\Gamma}] [\text{Inhabited } {\Gamma'}] (f : \text{PointedMap } {\Gamma} {\Gamma'}) (L R : \text{ListBlank } {\Gamma}),\ (Tape.map f (Tape.mk' L R)) = Tape.mk' (L.map f) (R.map f) $$$
Lean4
theorem map_mk' {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (L R : ListBlank Γ) :
(Tape.mk' L R).map f = Tape.mk' (L.map f) (R.map f) := by
simp only [Tape.mk', Tape.map, ListBlank.head_map, ListBlank.tail_map]
