fold_empty

Mathlib.Data.Finset.Fold

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

English

Folding over the empty finite set yields the seed value: fold op b f ∅ = b.

Русский

Свертка по пустому множеству даёт начальное значение: fold op b f ∅ = b.

LaTeX

$$$(\\emptyset : Finset\\; \\alpha).fold\\; op\\; b\\; f = b$$$

Lean4

@[simp]
theorem fold_empty : (∅ : Finset α).fold op b f = b :=
  rfl

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

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

Разделы

Аффилиация

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