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 [*]