Documentation

Mathlib.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 : IsCommutative β op] [ha : IsAssociative β 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
Instances For
    @[simp]
    theorem Finset.fold_empty {α : Type u_1} {β : Type u_2} {op : βββ} [hc : IsCommutative β op] [ha : IsAssociative β op] {f : αβ} {b : β} :
    Finset.fold op b f = b
    @[simp]
    theorem Finset.fold_cons {α : Type u_1} {β : Type u_2} {op : βββ} [hc : IsCommutative β op] [ha : IsAssociative β 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 : IsCommutative β op] [ha : IsAssociative β 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 : IsCommutative β op] [ha : IsAssociative β 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 : IsCommutative β op] [ha : IsAssociative β 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 : IsCommutative β op] [ha : IsAssociative β op] {f : αβ} {b : β} [DecidableEq α] {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 : IsCommutative β op] [ha : IsAssociative β 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 : IsCommutative β op] [ha : IsAssociative β 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 : IsCommutative β op] [ha : IsAssociative β 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 : IsCommutative β op] [ha : IsAssociative β op] {f : αβ} {b : β} {s : Finset α} {op' : γγγ} [IsCommutative γ op'] [IsAssociative γ 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 : IsCommutative β op] [ha : IsAssociative β op] {f : αβ} {s₁ : Finset α} {s₂ : Finset α} {b₁ : β} {b₂ : β} (h : Disjoint s₁ s₂) :
    Finset.fold op (op b₁ b₂) f (Finset.disjUnion s₁ 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 : IsCommutative β op] [ha : IsAssociative β op] {f : αβ} {ι : Type u_4} {s : Finset ι} {t : ιFinset α} {b : ιβ} {b₀ : β} (h : Set.PairwiseDisjoint (s) t) :
    Finset.fold op (Finset.fold op b₀ b s) f (Finset.disjiUnion s 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 : IsCommutative β op] [ha : IsAssociative β 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 : IsCommutative β op] [ha : IsAssociative β op] {f : αβ} {b : β} {s : Finset α} {a : α} [DecidableEq α] [hi : IsIdempotent β 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 : IsCommutative β op] [ha : IsAssociative β op] {f : αβ} {b : β} [DecidableEq α] {g : γα} {s : Finset γ} [hi : IsIdempotent β 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 : IsCommutative β op] [ha : IsAssociative β 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 : IsCommutative β op] [ha : IsAssociative β op] {f : αβ} {b : β} {s : Finset α} [IsIdempotent β 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 : IsCommutative β op] [ha : IsAssociative β 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 : IsCommutative β op] [ha : IsAssociative β 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)
    @[simp]
    theorem Finset.fold_union_empty_singleton {α : Type u_1} [DecidableEq α] (s : Finset α) :
    Finset.fold (fun x x_1 => x x_1) singleton s = s
    theorem Finset.fold_sup_bot_singleton {α : Type u_1} [DecidableEq α] (s : Finset α) :
    Finset.fold (fun x x_1 => x x_1) singleton s = s
    theorem Finset.le_fold_min {α : Type u_1} {β : Type u_2} {f : αβ} {b : β} {s : Finset α} [LinearOrder β] (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 α} [LinearOrder β] (c : β) :
    Finset.fold min b f s c b c x, x s f x c
    theorem Finset.lt_fold_min {α : Type u_1} {β : Type u_2} {f : αβ} {b : β} {s : Finset α} [LinearOrder β] (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 α} [LinearOrder β] (c : β) :
    Finset.fold min b f s < c b < c x, x s f x < c
    theorem Finset.fold_max_le {α : Type u_1} {β : Type u_2} {f : αβ} {b : β} {s : Finset α} [LinearOrder β] (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 α} [LinearOrder β] (c : β) :
    c Finset.fold max b f s c b x, x s c f x
    theorem Finset.fold_max_lt {α : Type u_1} {β : Type u_2} {f : αβ} {b : β} {s : Finset α} [LinearOrder β] (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 α} [LinearOrder β] (c : β) :
    c < Finset.fold max b f s c < b x, x s c < f x
    theorem Finset.fold_max_add {α : Type u_1} {β : Type u_2} {f : αβ} [LinearOrder β] [Add β] [CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (n : WithBot β) (s : Finset α) :
    Finset.fold max (fun x => ↑(f x) + n) s = Finset.fold max (WithBot.some f) s + n