English
For a relation r with r x (op y z) equivalent to r x y ∧ r x z, the relation between c and the fold over s reduces to a conjunction with b and all f x.
Русский
Если отношение r(x, op(y,z)) эквивалентно r(x,y) ∧ r(x,z), то связь между c и свёрткой по s сводится к конъюнкции с b и каждым f x.
LaTeX
$$$r c (s.fold op b f) \\iff r c b \\land \\forall x \\in s, r c (f x)$$$
Lean4
theorem fold_op_rel_iff_and {r : β → β → Prop} (hr : ∀ {x y z}, r x (op y z) ↔ r x y ∧ r x z) {c : β} :
r c (s.fold op b f) ↔ r c b ∧ ∀ x ∈ s, r c (f x) := by
classical
induction s using Finset.induction_on with
| empty => simp
| insert a s ha
IH =>
rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
simp
