fold_cons_left

Mathlib.Data.Multiset.Fold

URI: https://scilib.ai/kg/mathlib#Multiset.fold_cons_left

English

For all op, a, b, s, (a ::ₘ s).fold op b = op a (s.fold op b).

Русский

Для любой операции op и элементов a, b, s выполняется (a ::ₘ s).fold op b = op a (s.fold op b).

LaTeX

$$$ (a \;::_m\; s).\mathrm{fold} \ op \ b = \mathrm{op} \ a \ (s.\mathrm{fold} \ op \ b) $$$

Lean4

@[simp]
theorem fold_cons_left : ∀ (b a : α) (s : Multiset α), (a ::ₘ s).fold op b = a * s.fold op b :=
  foldr_cons _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru