fold_map — Mathlib

English

Folding over the mapped Finset s.map g is the same as folding over s with the composed function f ∘ g.

Русский

Свёртка по отображению s.map g эквивалентна свёртке по s с f ∘ g.

LaTeX

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

Lean4

@[simp]
theorem fold_map {g : γ ↪ α} {s : Finset γ} : (s.map g).fold op b f = s.fold op b (f ∘ g) := by
  simp only [fold, map, Multiset.map_map]

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