map_init — Mathlib

English

Mapping initialization commutes with list init: (init l).map f1 g1 = init (l.map f1).

Русский

Инициализация отображения совместима с операцией init: (init l).map f1 g1 = init (l.map f1).

LaTeX

$$$(\\mathrm{init}\\;l).\\mathrm{map}\\ f_1\\ g_1 = \\mathrm{init}\\ (l.\\mathrm{map}\\ f_1)$$$

Lean4

theorem map_init (g₁ : PointedMap Λ Λ') (l : List Γ) : (init l).map f₁ g₁ = init (l.map f₁) :=
  congr (congr_arg Cfg.mk g₁.map_pt) (Tape.map_mk₁ _ _)

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