The fold operation for a commutative associative operation over a finset. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
fold #
def
finset.fold
{α : Type u_1}
{β : Type u_2}
(op : β → β → β)
[hc : is_commutative β op]
[ha : is_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.
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_cons
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β}
{s : finset α}
{a : α}
(h : a ∉ s) :
finset.fold op b f (finset.cons a s h) = op (f a) (finset.fold op b f s)
@[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 α]
(h : 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 γ}
(H : ∀ (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 : α → β}
(H : ∀ (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_const
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{b : β}
{s : finset α}
[decidable (s = ∅)]
(c : β)
(h : op c (op b c) = op b c) :
finset.fold op b (λ (_x : α), c) s = ite (s = ∅) b (op b c)
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 : β → γ}
(hm : ∀ (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_disj_union
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{s₁ s₂ : finset α}
{b₁ b₂ : β}
(h : disjoint s₁ s₂) :
finset.fold op (op b₁ b₂) f (s₁.disj_union s₂ h) = op (finset.fold op b₁ f s₁) (finset.fold op b₂ f s₂)
theorem
finset.fold_disj_Union
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{ι : Type u_3}
{s : finset ι}
{t : ι → finset α}
{b : ι → β}
{b₀ : β}
(h : ↑s.pairwise_disjoint t) :
finset.fold op (finset.fold op b₀ b s) f (s.disj_Union t h) = finset.fold op b₀ (λ (i : ι), finset.fold op (b i) f (t i)) 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_image_idem
{α : 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 γ}
[hi : is_idempotent β op] :
finset.fold op b f (finset.image g s) = finset.fold op b (f ∘ g) s
theorem
finset.fold_ite'
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β}
{s : finset α}
{g : α → β}
(hb : op b b = b)
(p : α → Prop)
[decidable_pred p] :
finset.fold op b (λ (i : α), ite (p i) (f i) (g i)) s = op (finset.fold op b f (finset.filter p s)) (finset.fold op b g (finset.filter (λ (i : α), ¬p i) s))
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 : is_commutative β op]
[ha : is_associative β op]
{f : α → β}
{b : β}
{s : finset α}
[is_idempotent β op]
{g : α → β}
(p : α → Prop)
[decidable_pred p] :
finset.fold op b (λ (i : α), ite (p i) (f i) (g i)) s = op (finset.fold op b f (finset.filter p s)) (finset.fold op b g (finset.filter (λ (i : α), ¬p i) s))
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 : 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 : β} :
@[simp]
theorem
finset.le_fold_min
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[linear_order β]
(c : β) :
c ≤ finset.fold linear_order.min b f s ↔ c ≤ b ∧ ∀ (x : α), x ∈ s → c ≤ f x
theorem
finset.fold_min_le
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[linear_order β]
(c : β) :
finset.fold linear_order.min b f s ≤ c ↔ b ≤ c ∨ ∃ (x : α) (H : x ∈ s), f x ≤ c
theorem
finset.lt_fold_min
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[linear_order β]
(c : β) :
c < finset.fold linear_order.min b f s ↔ c < b ∧ ∀ (x : α), x ∈ s → c < f x
theorem
finset.fold_min_lt
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[linear_order β]
(c : β) :
finset.fold linear_order.min b f s < c ↔ b < c ∨ ∃ (x : α) (H : x ∈ s), f x < c
theorem
finset.fold_max_le
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[linear_order β]
(c : β) :
finset.fold linear_order.max b f s ≤ c ↔ b ≤ c ∧ ∀ (x : α), x ∈ s → f x ≤ c
theorem
finset.le_fold_max
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[linear_order β]
(c : β) :
c ≤ finset.fold linear_order.max b f s ↔ c ≤ b ∨ ∃ (x : α) (H : x ∈ s), c ≤ f x
theorem
finset.fold_max_lt
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[linear_order β]
(c : β) :
finset.fold linear_order.max b f s < c ↔ b < c ∧ ∀ (x : α), x ∈ s → f x < c
theorem
finset.lt_fold_max
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : finset α}
[linear_order β]
(c : β) :
c < finset.fold linear_order.max b f s ↔ c < b ∨ ∃ (x : α) (H : x ∈ s), c < f x
theorem
finset.fold_max_add
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[linear_order β]
[has_add β]
[covariant_class β β (function.swap has_add.add) has_le.le]
(n : with_bot β)
(s : finset α) :
finset.fold linear_order.max ⊥ (λ (x : α), ↑(f x) + n) s = finset.fold linear_order.max ⊥ (coe ∘ f) s + n