English
Let f: α → β and l be a list of α. Then the sublists of map f l are exactly obtained by mapping f over every sublist of l; i.e. sublists'(map f l) = map (map f) (sublists' l).
Русский
Пусть f: α → β и l — список элементов α. Тогда подсписки отображения f над l равны отображениям f над каждым подсписком l: sublists'(map f l) = map (map f) (sublists' l).
LaTeX
$$$$ \\mathrm{sublists}'(\\mathrm{map} f\\; l) = \\mathrm{map}(\\mathrm{map} f)\\; (\\mathrm{sublists}'\\; l) $$$$
Lean4
theorem sublists'_map (f : α → β) : ∀ (l : List α), sublists' (map f l) = map (map f) (sublists' l)
| [] => by simp
| a :: l => by simp [map_cons, sublists'_cons, sublists'_map f l, Function.comp]
