mathlib documentation

data.finset.fold

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] (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 sg x = g yx = 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 sf 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 : ∀ (a : α), a s₁a 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_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 sr 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 sc 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 sc < 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 sf 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 sf 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 α) :