English
A weaker version of fold_ite' relying on a global idempotent operation, distributing the fold across true/false parts of a predicate p.
Русский
Ослабленная версия fold_ite, зависящая от глобальной идемпотентности операции, распределяет свёртку по частям истинности/ложности предиката p.
LaTeX
$$$\\mathrm{fold}_{op}\\; b\\; (\\lambda i. \\mathrm{ite}(p(i))(f(i))(g(i)))\\ s = \\mathrm{op}( \\mathrm{fold}_{op}\\; b\\; f\\; (s\\cap \\{i: p(i)\\}), \\mathrm{fold}_{op}\\; b\\; g\\; (s\\cap \\{i: \\neg p(i)\\}) )$$$
Lean4
/-- A weaker version of `Finset.fold_ite'`,
relying on typeclass idempotency over the whole type,
instead of solely on the seed element.
However, this is easier to use because it does not generate side goals. -/
theorem fold_ite [Std.IdempotentOp op] {g : α → β} (p : α → Prop) [DecidablePred p] :
Finset.fold op b (fun i => ite (p i) (f i) (g i)) s =
op (Finset.fold op b f (s.filter p)) (Finset.fold op b g (s.filter fun i => ¬p i)) :=
fold_ite' (Std.IdempotentOp.idempotent _) _
