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.
Equations
- Finset.fold op b f s = Multiset.fold op b (Multiset.map f s.val)
Instances For
@[simp]
theorem
Finset.fold_empty
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : Std.Commutative op]
[ha : Std.Associative op]
{f : α → β}
{b : β}
:
Finset.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)
:
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 : Std.Commutative op]
[ha : Std.Associative op]
{f : α → β}
{b : β}
{s : Finset α}
{a : α}
[DecidableEq α]
(h : a ∉ s)
:
Finset.fold op b f (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 : Std.Commutative op]
[ha : Std.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 : Std.Commutative op]
[ha : Std.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 : Std.Commutative op]
[ha : Std.Associative op]
{f : α → β}
{b : β}
[DecidableEq α]
{g : γ → α}
{s : Finset γ}
(H : ∀ x ∈ s, ∀ 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 : Std.Commutative op]
[ha : Std.Associative op]
{f : α → β}
{b : β}
{s : Finset α}
{g : α → β}
(H : ∀ 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 : Std.Commutative op]
[ha : Std.Associative op]
{s : Finset α}
{f : α → β}
{g : α → β}
{b₁ : β}
{b₂ : β}
:
Finset.fold op (op b₁ b₂) (fun (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 : Std.Commutative op]
[ha : Std.Associative op]
{b : β}
{s : Finset α}
[hd : Decidable (s = ∅)]
(c : β)
(h : op c (op b c) = op b c)
:
Finset.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))
:
Finset.fold op' (m b) (fun (x : α) => m (f x)) s = m (Finset.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₁ : Finset α}
{s₂ : Finset α}
{b₁ : β}
{b₂ : β}
(h : Disjoint s₁ s₂)
:
Finset.fold op (op b₁ b₂) f (s₁.disjUnion s₂ h) = op (Finset.fold op b₁ f s₁) (Finset.fold op b₂ f s₂)
theorem
Finset.fold_disjiUnion
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : Std.Commutative op]
[ha : Std.Associative op]
{f : α → β}
{ι : Type u_4}
{s : Finset ι}
{t : ι → Finset α}
{b : ι → β}
{b₀ : β}
(h : (↑s).PairwiseDisjoint t)
:
Finset.fold op (Finset.fold op b₀ b s) f (s.disjiUnion t h) = Finset.fold op b₀ (fun (i : ι) => Finset.fold op (b i) f (t i)) s
theorem
Finset.fold_union_inter
{α : Type u_1}
{β : Type u_2}
{op : β → β → β}
[hc : Std.Commutative op]
[ha : Std.Associative op]
{f : α → β}
[DecidableEq α]
{s₁ : Finset α}
{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 : Std.Commutative op]
[ha : Std.Associative op]
{f : α → β}
{b : β}
{s : Finset α}
{a : α}
[DecidableEq α]
[hi : Std.IdempotentOp op]
:
Finset.fold op b f (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 : Std.Commutative op]
[ha : Std.Associative op]
{f : α → β}
{b : β}
[DecidableEq α]
{g : γ → α}
{s : Finset γ}
[hi : Std.IdempotentOp 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 : Std.Commutative op]
[ha : Std.Associative op]
{f : α → β}
{b : β}
{s : Finset α}
{g : α → β}
(hb : op b b = b)
(p : α → Prop)
[DecidablePred p]
:
Finset.fold op b (fun (i : α) => if p i then f i else g i) s = op (Finset.fold op b f (Finset.filter p s)) (Finset.fold op b g (Finset.filter (fun (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 : Std.Commutative op]
[ha : Std.Associative op]
{f : α → β}
{b : β}
{s : Finset α}
[Std.IdempotentOp op]
{g : α → β}
(p : α → Prop)
[DecidablePred p]
:
Finset.fold op b (fun (i : α) => if p i then f i else g i) s = op (Finset.fold op b f (Finset.filter p s)) (Finset.fold op b g (Finset.filter (fun (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 : 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 (Finset.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 (Finset.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 α)
:
Finset.fold (fun (x1 x2 : Finset α) => x1 ∪ x2) ∅ singleton s = s
theorem
Finset.fold_sup_bot_singleton
{α : Type u_1}
[DecidableEq α]
(s : Finset α)
:
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 : β)
:
theorem
Finset.fold_min_le
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : Finset α}
[LinearOrder β]
(c : β)
:
theorem
Finset.lt_fold_min
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : Finset α}
[LinearOrder β]
(c : β)
:
theorem
Finset.fold_min_lt
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : Finset α}
[LinearOrder β]
(c : β)
:
theorem
Finset.fold_max_le
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : Finset α}
[LinearOrder β]
(c : β)
:
theorem
Finset.le_fold_max
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : Finset α}
[LinearOrder β]
(c : β)
:
theorem
Finset.fold_max_lt
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : Finset α}
[LinearOrder β]
(c : β)
:
theorem
Finset.lt_fold_max
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{b : β}
{s : Finset α}
[LinearOrder β]
(c : β)
:
theorem
Finset.fold_max_add
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[LinearOrder β]
[Add β]
[CovariantClass β β (Function.swap fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 ≤ x2]
(n : WithBot β)
(s : Finset α)
:
Finset.fold max ⊥ (fun (x : α) => ↑(f x) + n) s = Finset.fold max ⊥ (WithBot.some ∘ f) s + n