English
If l is a list and comm makes f left-commutative on the elements of the corresponding multiset, then noncommFoldr f (l as multiset) comm b equals l.foldr f b.
Русский
Если l — список, и для элементов мультимножеств выполняется левое коммутативное свойство функции f, тогда noncommFoldr f (l как мультисет) comm b совпадает с l.foldr f b.
LaTeX
$$$\\mathrm{noncommFoldr}(f, (l:\\text{List}\\,\\alpha)\\text{ }comm, a) = l.\\text{foldr}(f, a).$$$
Lean4
@[simp]
theorem noncommFoldr_coe (l : List α) (comm) (b : β) : noncommFoldr f (l : Multiset α) comm b = l.foldr f b :=
by
simp only [noncommFoldr, coe_foldr, coe_attach, List.attach, List.attachWith, Function.comp_def]
rw [← List.foldr_map]
simp [List.map_pmap]
