Finset.prod_insertNone
theorem Finset.prod_insertNone :
∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] (f : Option α → M) (s : Finset α),
((Finset.insertNone s).prod fun x => f x) = f none * s.prod fun x => f (some x)
The theorem `Finset.prod_insertNone` states that for any given type `α` and a type `M` that forms a commutative monoid, and any function `f` from the optional type `Option α` to `M`, the product of the function `f` applied over the entire set obtained by inserting `none` into a finite set `s` of type `α` is equal to the product of `f none` and the product of `f` applied over the set `s` with every element wrapped into `some`. In other words, if we add a `none` value to a finite set and take the product over the whole set, it is the same as multiplying the function applied to `none` and the product over the original set with the function applied to each element wrapped into `some`.
More concisely: For any commutative monoid type M and function f from Option α to M, the product of f applied to the optional finite set obtained by inserting none into set s of type α is equal to the product of f none and the product of f applied to each some(x) in s, where x is an element of s.
|
Finset.sum_insertNone
theorem Finset.sum_insertNone :
∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : Option α → M) (s : Finset α),
((Finset.insertNone s).sum fun x => f x) = f none + s.sum fun x => f (some x)
The theorem `Finset.sum_insertNone` states that for any type `α`, Monoid `M` with addition (`AddCommMonoid M`), function `f` from an optional type `α` to `M`, and a finite set `s` of type `α`, the sum of function `f` applied on each element of the set obtained by inserting `none` into `s` (using the function `Finset.insertNone`), is equal to the sum of `f` applied to `none` plus the sum of function `f` applied on each element of the original set `s` after wrapping them with `some`. In other words, when summing over a set where `none` has been inserted, the contribution of `none` to the sum is exactly `f none` and the contribution of the other elements is as though `none` had not been inserted.
More concisely: For any Monoid `M` with addition, function `f` from an optional type `α` to `M`, and finite set `s` of type `α`, we have `Sum.sum (λx => if h : x ≠ none then some (f x) else none) (Finset.insertNone s) = some (f none) + Sum.sum (λx => f (some x)) s`.
|