English
If g : γ → α is injective on s, then folding over image g equals folding over s with f ∘ g.
Русский
Если g инъективно отображает s в α, то свёртка по image g равна свёртке по s с f ∘ g.
LaTeX
$$$\\mathrm{fold}_{op}\\; b\\; f\\; (\\mathrm{image}\\ g\\ s) = \\mathrm{fold}_{op}\\; b\\; (f \\circ g)\\; s$$$
Lean4
@[simp]
theorem fold_image [DecidableEq α] {g : γ → α} {s : Finset γ} (H : Set.InjOn g s) :
(s.image g).fold op b f = s.fold op b (f ∘ g) := by simp only [fold, image_val_of_injOn H, Multiset.map_map]