English
For every list l, the list obtained by applying pure to each element of l is a sublist of the list of all sublists of l.
Русский
Для каждого списка l список, полученный применением чистого к каждому элементу l, является подсписком списка всех подсписков l.
LaTeX
$$$\\operatorname{map} \\text{pure} \\, l <+ \\operatorname{sublists}(l)$$$
Lean4
theorem map_pure_sublist_sublists (l : List α) : map pure l <+ sublists l :=
by
induction l using reverseRecOn <;> simp only [map, map_append, sublists_concat]
· simp only [sublists_nil, sublist_cons_self]
case append_singleton l a ih =>
exact
((append_sublist_append_left _).2 <|
singleton_sublist.2 <| mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by rfl⟩).trans
((append_sublist_append_right _).2 ih)
