English
For any m ∈ Multiset α and s ∈ Multiset (Multiset α), the sections of (m :: s) are obtained by taking each a ∈ m and prepending a to each section of s.
Русский
Для любых m ∈ Multiset α и s ∈ Multiset (Multiset α) разделы (m :: s) получаются путём взятия каждого элемента a из m и взвешивания его перед каждым разбором разделов из s.
LaTeX
$$$$ \\operatorname{Sections}(m :: s) = m \\;\\operatorname{bind}\\; (\\lambda a. \\operatorname{Sections}(s) \\;\\operatorname{map}\\; (\\operatorname{Multiset.cons} \\, a)). $$$$
Lean4
@[simp]
theorem sections_cons (s : Multiset (Multiset α)) (m : Multiset α) :
Sections (m ::ₘ s) = m.bind fun a => (Sections s).map (Multiset.cons a) :=
recOn_cons m s
