map_inits — Mathlib

English

For any g, mapping g over l preserves the inits up to mapping, i.e. (l.map g).inits = l.inits.map (map g).

Русский

Покрытие отображением g сохраняет иниты: (l.map g).inits = l.inits.map (map g).

LaTeX

$$$(\\operatorname{map} g\; l).\\operatorname{inits} = \\operatorname{inits} l.\\operatorname{map}(\\operatorname{map} g)$$$

Lean4

theorem map_inits {β : Type*} (g : α → β) : (l.map g).inits = l.inits.map (map g) := by
  induction l using reverseRecOn <;> simp [*]

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