fold_op_rel_iff_or — Mathlib

English

If r x (op y z) is equivalent to r x y ∨ r x z, then r c (s.fold op b f) is equivalent to r c b ∨ ∃ x ∈ s, r c (f x).

Русский

Если r x (op y z) эквивалентно r x y ∨ r x z, тогда r c (s.fold op b f) эквивалентно r c b ∨ ∃ x ∈ s, r c (f x).

LaTeX

$$$r c (s.fold op b f) \\iff r c b \\lor \\exists x \\in s, r c (f x)$$$

Lean4

theorem fold_op_rel_iff_or {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, ← or_assoc, @or_comm (r c (f a)), or_assoc]
    simp

Похожие утверждения