Lemmas about products and sums over finite sets in Option α #
In this file we prove formulas for products and sums over Finset.insertNone s and
Finset.eraseNone s.
theorem
Finset.prod_insertNone
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
(f : Option α → M)
(s : Finset α)
:
Eq ((DFunLike.coe insertNone s).prod fun (x : Option α) => f x)
(HMul.hMul (f Option.none) (s.prod fun (x : α) => f (Option.some x)))
theorem
Finset.sum_insertNone
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
(f : Option α → M)
(s : Finset α)
:
Eq ((DFunLike.coe insertNone s).sum fun (x : Option α) => f x)
(HAdd.hAdd (f Option.none) (s.sum fun (x : α) => f (Option.some x)))
theorem
Finset.mul_prod_eq_prod_insertNone
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
(f : α → M)
(x : M)
(s : Finset α)
:
Eq (HMul.hMul x (s.prod fun (i : α) => f i)) ((DFunLike.coe insertNone s).prod fun (i : Option α) => i.elim x f)
theorem
Finset.add_sum_eq_sum_insertNone
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
(f : α → M)
(x : M)
(s : Finset α)
:
Eq (HAdd.hAdd x (s.sum fun (i : α) => f i)) ((DFunLike.coe insertNone s).sum fun (i : Option α) => i.elim x f)
theorem
Finset.prod_eraseNone
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
(f : α → M)
(s : Finset (Option α))
:
Eq ((DFunLike.coe eraseNone s).prod fun (x : α) => f x) (s.prod fun (x : Option α) => Option.elim' 1 f x)
theorem
Finset.sum_eraseNone
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
(f : α → M)
(s : Finset (Option α))
:
Eq ((DFunLike.coe eraseNone s).sum fun (x : α) => f x) (s.sum fun (x : Option α) => Option.elim' 0 f x)