fold — Mathlib

English

Fold op b f s folds a commutative associative operation over the f-image of s, i.e., fold op b f {1,2,3} = f(1) ∘ f(2) ∘ f(3) ∘ b.

Русский

Свертка по Finset: свёртка OP над изображением f множества s даёт последовательность f(х) для х ∈ s, начиная с b.

LaTeX

$$$\\mathrm{fold}_{op}\\; b\\; f\\; s = (s.1.map\\; f).fold\\; op\\; b$$$

Lean4

/-- `fold op b f s` folds the commutative associative operation `op` over the
  `f`-image of `s`, i.e. `fold (+) b f {1,2,3} = f 1 + f 2 + f 3 + b`. -/
def fold (b : β) (f : α → β) (s : Finset α) : β :=
  (s.1.map f).fold op b

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