English
A stronger version of fold_ite' with explicit handling of a predicate p, distributing the fold across p-filtered and its complement, under idempotency assumptions.
Русский
Усиленная версия 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\\setminus \\{i\\mid p(i)\\})) \\; (\\mathrm{fold}_{op}\\; b\\; g\\; (s\\{i\\mid \\neg p(i)\\}))$$$
Lean4
/-- A stronger version of `Finset.fold_ite`, but relies on
an explicit proof of idempotency on the seed element, rather
than relying on typeclass idempotency over the whole type. -/
theorem fold_ite' {g : α → β} (hb : op b b = b) (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)) :=
by
classical
induction s using Finset.induction_on with
| empty => simp [hb]
| insert x s hx IH =>
simp only [Finset.fold_insert hx]
split_ifs with h
· have : x ∉ Finset.filter p s := by simp [hx]
simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
· have : x ∉ Finset.filter (fun i => ¬p i) s := by simp [hx]
simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
