English
For a constant value c and a rule op c (op b c) = op b c, the folding with a constant function reduces to a conditional depending on emptiness.
Русский
Для константы c и условия op c (op b c) = op b c свёртка константной функции зависит от пустоты множества.
LaTeX
$$$\\text{fold op b (\\u2192) c s = if s = ∅ then b else op b c}$$$
Lean4
theorem fold_const [hd : Decidable (s = ∅)] (c : β) (h : op c (op b c) = op b c) :
Finset.fold op b (fun _ => c) s = if s = ∅ then b else op b c := by
classical
induction s using Finset.induction_on generalizing hd with
| empty => simp
| insert x s hx IH =>
simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
split_ifs
· rw [hc.comm]
· exact h
