map_mk₁ — Mathlib

English

The map of Mk₁ is obtained by mapping over Mk₂ of two lists: (Tape.mk₁ l).map f = Tape.mk₁ (l.map f).

Русский

Отображение Mk₁ эквивалентно отображению Mk₂ двух списков: (Tape.mk₁ l).map f = Tape.mk₁ (l.map f).

LaTeX

$$$ \forall {\Gamma} {\Gamma'} [\text{Inhabited } {\Gamma}] [\text{Inhabited } {\Gamma'}] (f : \text{PointedMap } {\Gamma} {\Gamma'}) (l : \text{List } {\Gamma}),\ (Tape.map f (Tape.mk₁ l)) = Tape.mk₁ (List.map f.f l) $$$

Lean4

theorem map_mk₁ {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : List Γ) :
    (Tape.mk₁ l).map f = Tape.mk₁ (l.map f) :=
  Tape.map_mk₂ _ _ _

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