English
If op is idempotent, folding over image g preserves the same fold as folding over s with f ∘ g.
Русский
Если op идемпотентна, свёртка по изображению g сохраняет ту же свёртку, что и свёртка по s с f ∘ g.
LaTeX
$$$(image\\ g\\ s).fold op b f = s.fold op b (f \\circ g)$$$
Lean4
theorem fold_image_idem [DecidableEq α] {g : γ → α} {s : Finset γ} [hi : Std.IdempotentOp op] :
(image g s).fold op b f = s.fold op b (f ∘ g) := by
induction s using Finset.cons_induction with
| empty => rw [fold_empty, image_empty, fold_empty]
| cons x xs hx ih =>
haveI := Classical.decEq γ
rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
simp only [Function.comp_apply]
