The fold operation for a commutative associative operation over a finset.
fold
def
finset.fold
{α : Type u_1}
{β : Type u_2}
(op : β → β → β)
[hc : is_commutative β op]
[ha : is_associative β op] :
β → (α → β) → 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`.
Equations
- finset.fold op b f s = multiset.fold op b (multiset.map f s.val)
@[simp]
theorem
finset.fold_empty
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β} :
finset.fold op b f ∅ = b
@[simp]
theorem
finset.fold_insert
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β}
{s : finset α}
{a : α}
[decidable_eq α] :
a ∉ s → finset.fold op b f (has_insert.insert a s) = op (f a) (finset.fold op b f s)
@[simp]
theorem
finset.fold_singleton
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β}
{a : α} :
finset.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 : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β}
{g : γ ↪ α}
{s : finset γ} :
finset.fold op b f (finset.map g s) = finset.fold op b (f ∘ ⇑g) s
@[simp]
theorem
finset.fold_image
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β}
[decidable_eq α]
{g : γ → α}
{s : finset γ} :
(∀ (x : γ), x ∈ s → ∀ (y : γ), y ∈ s → g x = g y → x = y) → finset.fold op b f (finset.image g s) = finset.fold op b (f ∘ g) s
theorem
finset.fold_congr
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β}
{s : finset α}
{g : α → β} :
(∀ (x : α), x ∈ s → f x = g x) → finset.fold op b f s = finset.fold op b g s
theorem
finset.fold_op_distrib
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{s : finset α}
{f g : α → β}
{b₁ b₂ : β} :
finset.fold op (op b₁ b₂) (λ (x : α), op (f x) (g x)) s = op (finset.fold op b₁ f s) (finset.fold op b₂ g s)
theorem
finset.fold_hom
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β}
{s : finset α}
{op' : γ → γ → γ}
[is_commutative γ op']
[is_associative γ op']
{m : β → γ} :
(∀ (x y : β), m (op x y) = op' (m x) (m y)) → finset.fold op' (m b) (λ (x : α), m (f x)) s = m (finset.fold op b f s)
theorem
finset.fold_union_inter
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
[decidable_eq α]
{s₁ s₂ : finset α}
{b₁ b₂ : β} :
op (finset.fold op b₁ f (s₁ ∪ s₂)) (finset.fold op b₂ f (s₁ ∩ s₂)) = op (finset.fold op b₂ f s₁) (finset.fold op b₁ f s₂)
@[simp]
theorem
finset.fold_insert_idem
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β}
{s : finset α}
{a : α}
[decidable_eq α]
[hi : is_idempotent β op] :
finset.fold op b f (has_insert.insert a s) = op (f a) (finset.fold op b f s)
theorem
finset.fold_op_rel_iff_and
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_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 (finset.fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
theorem
finset.fold_op_rel_iff_or
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_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 (finset.fold op b f s) ↔ r c b ∨ ∃ (x : α) (H : x ∈ s), r c (f x)
theorem
finset.le_fold_min
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[decidable_linear_order β]
(c : β) :
theorem
finset.fold_min_le
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[decidable_linear_order β]
(c : β) :
theorem
finset.lt_fold_min
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[decidable_linear_order β]
(c : β) :
theorem
finset.fold_min_lt
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[decidable_linear_order β]
(c : β) :
theorem
finset.fold_max_le
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[decidable_linear_order β]
(c : β) :
theorem
finset.le_fold_max
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[decidable_linear_order β]
(c : β) :
theorem
finset.fold_max_lt
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[decidable_linear_order β]
(c : β) :
theorem
finset.lt_fold_max
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[decidable_linear_order β]
(c : β) :