mathlib3 documentation

data.finset.fold

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
@[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 : β} :
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 α} [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 α) :