fold_singleton

Mathlib.Data.Finset.Fold

URI: https://scilib.ai/kg/mathlib#Finset.fold_singleton

English

Folding over a singleton {a} yields op(f(a), b).

Русский

Свёртка по множесту-одиночке даёт op(f(a), b).

LaTeX

$$$\\mathrm{fold}_{op}\\; b\\; f\\; (\\{a\\}) = op(f(a), b)$$$

Lean4

@[simp]
theorem fold_singleton : ({ a } : Finset α).fold op b f = f a * b :=
  rfl

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

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

Разделы

Аффилиация

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