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.
@[simp]
theorem
Finset.sum_insertNone
{α : Type u_1}
{M : Type u_2}
[inst : AddCommMonoid M]
(f : Option α → M)
(s : Finset α)
:
(Finset.sum (↑Finset.insertNone.toEmbedding s) fun x => f x) = f none + Finset.sum s fun x => f (some x)
@[simp]
theorem
Finset.prod_insertNone
{α : Type u_1}
{M : Type u_2}
[inst : CommMonoid M]
(f : Option α → M)
(s : Finset α)
:
(Finset.prod (↑Finset.insertNone.toEmbedding s) fun x => f x) = f none * Finset.prod s fun x => f (some x)
theorem
Finset.sum_eraseNone
{α : Type u_1}
{M : Type u_2}
[inst : AddCommMonoid M]
(f : α → M)
(s : Finset (Option α))
:
(Finset.sum (↑Finset.eraseNone s) fun x => f x) = Finset.sum s fun x => Option.elim' 0 f x
theorem
Finset.prod_eraseNone
{α : Type u_1}
{M : Type u_2}
[inst : CommMonoid M]
(f : α → M)
(s : Finset (Option α))
:
(Finset.prod (↑Finset.eraseNone s) fun x => f x) = Finset.prod s fun x => Option.elim' 1 f x