Finset.fold_op_rel_iff_or
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},
(∀ {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)
The theorem `Finset.fold_op_rel_iff_or` states that for any types `α` and `β`, a binary operation `op` on `β` that is commutative and associative, a function `f` from `α` to `β`, a base value `b` of type `β`, a finite set `s` of type `α`, and a binary relation `r` on `β`, if the relation `r` satisfies the property that `r x (op y z)` is equivalent to `r x y` or `r x z` for all `x`, `y`, `z` of type `β`, then the relation `r c (Finset.fold op b f s)` is equivalent to `r c b` or there exists an `x` in `s` such that `r c (f x)` holds for any `c` of type `β`. In other words, the relationship `r` holds between `c` and the fold of `s` through `op` and `f` if and only if it holds between `c` and `b`, or there exists an element `x` in `s` for which the relationship `r` holds after applying `f` to `x`.
More concisely: For any commutative and associative binary operation `op` on type `β`, function `f` from `α` to `β`, base value `b` of type `β`, binary relation `r` on `β`, and finite set `s` of type `α`, if `r` satisfies `r x (op y z) ↔ r x y ∨ r x z` for all `x, y, z` in `β`, then `r c (Finset.fold op b f s) ↔ r c b ∨ ∃x ∈ s, r c (f x)`.
|
Finset.fold_cons
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)
The theorem `Finset.fold_cons` states that for any types `α` and `β`, any commutative and associative operation `op` on `β`, any function `f` from `α` to `β`, any base element `b` of type `β`, any finite set `s` of elements of type `α`, and any element `a` of type `α` not in `s`, applying the `Finset.fold` operation to the set obtained by adding `a` to `s` (i.e., `Finset.cons a s h`) is the same as applying the operation `op` to `f(a)` and the result of folding `op` over `s`. In mathematical terms, it means if we have a set `{a} ∪ s` and we fold an operation over this set, it's the same as applying the operation to `f(a)` and the result of folding the operation over the original set `s`.
More concisely: For any commutative and associative operation `op` on type `β`, function `f` from `α` to `β`, base element `b` of type `β`, finite set `s` of elements of type `α`, and element `a` of type `α` not in `s`, we have `Finset.fold op (Finset.cons a s h) f b = op (f a) (Finset.fold op s f b)`.
|
Finset.fold_ite
theorem Finset.fold_ite :
∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β}
{b : β} {s : Finset α} [inst : Std.IdempotentOp op] {g : α → β} (p : α → Prop) [inst : 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))
This theorem, `Finset.fold_ite`, states that for any two types `α` and `β`, a binary operation `op` on `β` which is commutative and associative, a function `f` from `α` to `β`, a baseline value `b` of type `β`, a set `s` of elements of type `α`, and another function `g` from `α` to `β`, given a predicate `p` on `α` and the operation `op` is idempotent, the result of applying the fold operation on `s` with the function that applies `f` to the elements that satisfy `p` and `g` to the elements that do not, is equal to the operation `op` applied to the result of the fold operation on the elements of `s` that satisfy `p` using `f` and the result of the fold operation on the elements of `s` that do not satisfy `p` using `g`. This is a generalization of the concept of splitting a fold operation based on a predicate and can be useful in various contexts in functional programming and formal proofs.
More concisely: For any commutative, associative binary operation `op` on type `β`, function `f` from `α` to `β`, baseline value `b` of type `β`, set `s` of elements of type `α`, function `g` from `α` to `β`, and predicate `p` on `α`, if `op` is idempotent: `(Finset.fold op f b (Filter.filter p s) ++ Finset.fold op g b (Set.complement (Filter.filter p s))) = Finset.fold op (λ x => if h x then f x else g x) b s`, where `++` denotes set union and `h` is the decision function for `p`.
|
Finset.fold_insert_idem
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 : α} [inst : DecidableEq α] [hi : Std.IdempotentOp op],
Finset.fold op b f (insert a s) = op (f a) (Finset.fold op b f s)
The theorem `Finset.fold_insert_idem` states that for any types `α` and `β`, a binary operation `op` on `β` that is commutative and associative, a function `f` from `α` to `β`, a base value `b` of type `β`, a finite set `s` of type `α`, and an element `a` of type `α` where `α` has decidable equality and `op` is idempotent, the result of folding `op` over the `f`-image of the set obtained by inserting `a` into `s` starting from `b` is equal to applying `op` to `f(a)` and the result of folding `op` over the `f`-image of `s` starting from `b`. In simpler terms, it means that inserting an element into a set and then folding a commutative, associative and idempotent operation doesn't change the result compared to applying the operation to the element's image and the original fold operation.
More concisely: For any commutative, associative, idempotent binary operation `op` on type `β`, function `f` from type `α` to `β`, base value `b` of type `β`, finite set `s` of type `α` with decidable equality, and element `a` of type `α`, the following equality holds: `op.fold s (f a) b = op.fold (Finset.insert a s) b ⊕ f a`.
|
Finset.fold_congr
theorem Finset.fold_congr :
∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β}
{b : β} {s : Finset α} {g : α → β}, (∀ x ∈ s, f x = g x) → Finset.fold op b f s = Finset.fold op b g s
The theorem `Finset.fold_congr` states that for any types `α` and `β`, any commutative and associative operation `op` on `β`, any functions `f` and `g` from `α` to `β`, any base value `b` of type `β`, and any finite set `s` of elements of `α`, if for all elements `x` in `s`, `f x` equals `g x`, then the operation `op` folded over the `f`-image of `s` plus `b` equals the operation `op` folded over the `g`-image of `s` plus `b`. In other words, if two functions agree on all elements of a particular finite set, then folding a binary operation (that is commutative and associative) over the images of the set under each function (plus a certain base value) will give the same result.
More concisely: For any commutative and associative operation `op` on type `β`, functions `f` and `g` from `α` to `β`, base value `b` of type `β`, and finite set `s` of elements of `α`, if `f x = g x` for all `x` in `s`, then `op (∑ i in s, f i) b = op (∑ i in s, g i) b`.
|
Finset.fold_op_rel_iff_and
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},
(∀ {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)
This theorem states that for any types `α` and `β`, any commutative associative operation `op` on `β`, any function `f` from `α` to `β`, any elements `b` and `c` of `β`, any finset `s` of `α`, and any binary relation `r` on `β`, assuming the property that for all `x`, `y`, and `z` in `β`, `r x` holds on the operation of `y` and `z` if and only if `r x` holds on `y` and `r x` holds on `z`, then `r c` holds on the fold of `op` over the `f`-image of `s` with base `b` if and only if `r c` holds on `b` and for all `x` in `s`, `r c` holds on `f x`. In mathematical terms, \( r(c, \text{fold}\,op\,b\,f\,s) \) is equivalent to \( r(c, b) \) and \( \forall x\, \in s, r(c, f(x)) \).
More concisely: For any commutative associative operation `op` on type `β`, function `f` from `α` to `β`, and binary relation `r` satisfying the given condition, `r` holds on the fold of `op` over the `f`-image of a finite set `s` with base `b` if and only if it holds on `b` and for all `x` in `s`, `r` holds on `f(x)`.
|
Finset.fold_ite'
theorem Finset.fold_ite' :
∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β}
{b : β} {s : Finset α} {g : α → β},
op b b = b →
∀ (p : α → Prop) [inst : 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))
This theorem, named `Finset.fold_ite'`, establishes a stronger version of `Finset.fold_ite`. The theorem is about a specific operation `op` on a set of elements from a finite set `s` of type `α` mapped to type `β` by two functions `f` and `g`. The operation `op` is assumed to be commutative and associative. The theorem holds if the operation `op` is idempotent on a seed element `b`, i.e., `op b b = b`. For any decidable predicate `p`, the fold of `op` over `s` where each element `i` is mapped to `f i` if `p i` holds and `g i` otherwise, is equal to the operation `op` applied to the fold of `op` over the elements of `s` satisfying `p` (mapped by `f`), and the fold of `op` over the elements of `s` not satisfying `p` (mapped by `g`). In mathematical terms, this theorem essentially states that for specific types of operations and mappings, you can separate the elements of a set based on a predicate and process them separately.
More concisely: For a commutative, associative, and idempotent operation `op` on a finite set `s` of type `α` mapped to type `β`, and given decidable predicate `p` on `s`, the fold of `op` over `s` conditioned on `p` equals the operation `op` applied to the folds of `op` over `p`-satisfying and `p`-violating elements of `s`.
|
Finset.fold_insert
theorem Finset.fold_insert :
∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β}
{b : β} {s : Finset α} {a : α} [inst : DecidableEq α],
a ∉ s → Finset.fold op b f (insert a s) = op (f a) (Finset.fold op b f s)
The theorem `Finset.fold_insert` asserts that, for any types `α` and `β`, a binary operation `op` on `β` that is both commutative and associative, a function `f` from `α` to `β`, a base value `b` of type `β`, a finite set `s` of type `α`, and an element `a` of type `α` such that `a` is not in `s`, when we insert `a` into `s` and then fold `op` over the `f`-image of the resulting set starting with `b`, we get the same result as applying `op` to `f(a)` and the result of folding `op` over the `f`-image of `s` starting with `b`. This assumes that the equality for `α` is decidable. In other words, this says the result of the folding operation is not affected by the order of elements in the set.
More concisely: For any commutative and associative binary operation `op` on type `β`, function `f` from `α` to `β`, base value `b` of type `β`, finite set `s` of type `Finset α`, and element `a` not in `s`, the following equality holds: `(foldl op f b (insert a s)) = op (f a) (foldl op f b s)`.
|
Finset.fold_empty
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
The `Finset.fold_empty` theorem states that for any types `α` and `β`, any binary operation `op` on `β` that is both commutative and associative, any function `f` from `α` to `β`, and any element `b` of `β`, the fold of the operation `op` over the `f`-image of an empty finset with the initial value `b` is equal to `b`. In mathematical notation, this can be written as `fold(op, b, f, ∅) = b`. In short, applying a fold operation on an empty set always returns the initial value.
More concisely: For any commutative and associative binary operation `op` on type `β`, function `f` from `α` to `β`, and element `b` of `β`, the fold of `op` over the empty finset `∅` using `f` and `b` as arguments equals `b`. In mathematical notation, `fold(op, b, f, ∅) = b`.
|