map_mk₂ — Mathlib

English

Mapping a tape Mk₂ L R is the same as Mk₂ of the mapped lists L and R.

Русский

Отображение ленты Mk₂ L R эквивалентно Mk₂ отображения списков L и R.

LaTeX

$$$ \forall {\Gamma} {\Gamma'} [\text{Inhabited } {\Gamma}] [\text{Inhabited } {\Gamma'}] (f : \text{PointedMap } {\Gamma} {\Gamma'}) (L R : \text{List } {\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 : List Γ) :
    (Tape.mk₂ L R).map f = Tape.mk₂ (L.map f) (R.map f) := by simp only [Tape.mk₂, Tape.map_mk', ListBlank.map_mk]

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