The fold operation for a commutative associative operation over a finset.

fold

def Finset.fold {α : Type u_1} {β : Type u_2} (op : β → β → β) [hc : Std.Commutative op] [ha : Std.Associative op] (b : β) (f : α → β) (s : Finset α) : β

fold op b f s folds the commutative associative operation op over the f-image of s, i.e. fold (+) b f {1,2,3} = f 1 + f 2 + f 3 + b.

@[simp]

theorem Finset.fold_empty {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} : fold op b f ∅ = b

@[simp]

theorem Finset.fold_cons {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {s : Finset α} {a : α} (h : a ∉ s) : fold op b f (cons a s h) = op (f a) (fold op b f s)

@[simp]

theorem Finset.fold_insert {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {s : Finset α} {a : α} [DecidableEq α] (h : a ∉ s) : fold op b f (insert a s) = op (f a) (fold op b f s)

@[simp]

theorem Finset.fold_singleton {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {a : α} : fold op b f {a} = op (f a) b

@[simp]

theorem Finset.fold_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {g : γ ↪ α} {s : Finset γ} : fold op b f (map g s) = fold op b (f ∘ ⇑g) s

@[simp]

theorem Finset.fold_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} [DecidableEq α] {g : γ → α} {s : Finset γ} (H : Set.InjOn g ↑s) : fold op b f (image g s) = fold op b (f ∘ g) s

theorem Finset.fold_congr {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {s : Finset α} {g : α → β} (H : ∀ x ∈ s, f x = g x) : fold op b f s = fold op b g s

theorem Finset.fold_op_distrib {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {s : Finset α} {f g : α → β} {b₁ b₂ : β} : fold op (op b₁ b₂) (fun (x : α) => op (f x) (g x)) s = op (fold op b₁ f s) (fold op b₂ g s)

theorem Finset.fold_const {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {b : β} {s : Finset α} [hd : Decidable (s = ∅)] (c : β) (h : op c (op b c) = op b c) : fold op b (fun (x : α) => c) s = if s = ∅ then b else op b c

theorem Finset.fold_hom {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {s : Finset α} {op' : γ → γ → γ} [Std.Commutative op'] [Std.Associative op'] {m : β → γ} (hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)) : fold op' (m b) (fun (x : α) => m (f x)) s = m (fold op b f s)

theorem Finset.fold_disjUnion {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {s₁ s₂ : Finset α} {b₁ b₂ : β} (h : Disjoint s₁ s₂) : fold op (op b₁ b₂) f (s₁.disjUnion s₂ h) = op (fold op b₁ f s₁) (fold op b₂ f s₂)

theorem Finset.fold_union_inter {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} [DecidableEq α] {s₁ s₂ : Finset α} {b₁ b₂ : β} : op (fold op b₁ f (s₁ ∪ s₂)) (fold op b₂ f (s₁ ∩ s₂)) = op (fold op b₂ f s₁) (fold op b₁ f s₂)

@[simp]

theorem Finset.fold_insert_idem {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {s : Finset α} {a : α} [DecidableEq α] [hi : Std.IdempotentOp op] : fold op b f (insert a s) = op (f a) (fold op b f s)

theorem Finset.fold_image_idem {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} [DecidableEq α] {g : γ → α} {s : Finset γ} [hi : Std.IdempotentOp op] : fold op b f (image g s) = fold op b (f ∘ g) s

theorem Finset.fold_ite' {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {s : Finset α} {g : α → β} (hb : op b b = b) (p : α → Prop) [DecidablePred p] : fold op b (fun (i : α) => if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))

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 Finset.fold_ite {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {s : Finset α} [Std.IdempotentOp op] {g : α → β} (p : α → Prop) [DecidablePred p] : fold op b (fun (i : α) => if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))

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 Finset.fold_op_rel_iff_and {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {s : Finset α} {r : β → β → Prop} (hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z) {c : β} : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)

theorem Finset.fold_op_rel_iff_or {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {s : Finset α} {r : β → β → Prop} (hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z) {c : β} : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)

@[simp]

theorem Finset.fold_union_empty_singleton {α : Type u_1} [DecidableEq α] (s : Finset α) : fold (fun (x1 x2 : Finset α) => x1 ∪ x2) ∅ singleton s = s

theorem Finset.fold_sup_bot_singleton {α : Type u_1} [DecidableEq α] (s : Finset α) : fold (fun (x1 x2 : Finset α) => x1 ⊔ x2) ⊥ singleton s = s

theorem Finset.le_fold_min {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [LinearOrder β] (c : β) : c ≤ fold min b f s ↔ c ≤ b ∧ ∀ x ∈ s, c ≤ f x

theorem Finset.fold_min_le {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [LinearOrder β] (c : β) : fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

theorem Finset.lt_fold_min {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [LinearOrder β] (c : β) : c < fold min b f s ↔ c < b ∧ ∀ x ∈ s, c < f x

theorem Finset.fold_min_lt {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [LinearOrder β] (c : β) : fold min b f s < c ↔ b < c ∨ ∃ x ∈ s, f x < c

theorem Finset.fold_max_le {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [LinearOrder β] (c : β) : fold max b f s ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

theorem Finset.le_fold_max {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [LinearOrder β] (c : β) : c ≤ fold max b f s ↔ c ≤ b ∨ ∃ x ∈ s, c ≤ f x

theorem Finset.fold_max_lt {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [LinearOrder β] (c : β) : fold max b f s < c ↔ b < c ∧ ∀ x ∈ s, f x < c

theorem Finset.lt_fold_max {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [LinearOrder β] (c : β) : c < fold max b f s ↔ c < b ∨ ∃ x ∈ s, c < f x