map_tails

Mathlib.Data.List.Infix

URI: https://scilib.ai/kg/mathlib#List.map_tails

English

For any g, (l.map g).tails = l.tails.map (map g).

Русский

Для отображения g на список, хвосты отображаются как map g по хвостам.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru