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] :
β → (α → β)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_insert {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : is_commutative β op] [ha : is_associative β op] {f : α → β} {b : β} {s : finset α} {a : α} [decidable_eq α] :
a sfinset.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 : 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 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 : α → β} :
(∀ (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_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 (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 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)

@[simp]

theorem finset.le_fold_min {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : finset α} [linear_order β] (c : β) :
c finset.fold 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 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 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 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 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 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 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 max b f s c < b ∃ (x : α) (H : x s), c < f x