English
For every list ℓ of lists, Sections mapped from lists to multisets equals the mapping of the sections of ℓ to multisets.
Русский
Для любого списка ℓ списков разделы, получаемые путём отображения каждого внутреннего списка в мультисет, равны отображению разделов ℓ в мультисеты.
LaTeX
$$$$ \\operatorname{Sections}\\big( \\operatorname{l.map}(\\lambda l. (l : \\text{Multiset } \\alpha)) \\big) = \\operatorname{l.sections}.\\operatorname{map}(\\lambda l. (l : \\text{Multiset } \\alpha)) $$$$
Lean4
theorem coe_sections :
∀ l : List (List α),
Sections (l.map fun l : List α => (l : Multiset α) : Multiset (Multiset α)) =
(l.sections.map fun l : List α => (l : Multiset α) : Multiset (Multiset α))
| [] => rfl
| a :: l => by
simp only [List.map_cons, List.sections]
rw [← cons_coe, sections_cons, bind_map_comm, coe_sections l]
simp [Function.comp_def, List.flatMap]
