fold_eq_foldl — Mathlib

English

For a commutative and associative operation op, and b, s, we have fold op b s = foldl op b s for multisets s.

Русский

Для коммутативной и ассоциативной операции op и элемента b, для мультимножества s выполняется fold op b s = foldl op b s.

LaTeX

$$$ \forall {\alpha} {\beta}, \ OP \text{ (выполнение) } (\text{fold op b s}) = (\text{foldl op b s}) $$$

Lean4

theorem fold_eq_foldl (b : α) (s : Multiset α) : fold op b s = foldl op b s :=
  Quot.inductionOn s fun _ => coe_fold_l _ _ _

Похожие утверждения