Sums in WithTop #
This file proves results about finite sums over monoids extended by a bottom or top element.
@[simp]
theorem
WithTop.coe_sum
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
(s : Finset ι)
(f : ι → α)
:
↑(Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => ↑(f i)
theorem
WithTop.sum_eq_top_iff
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
{s : Finset ι}
{f : ι → WithTop α}
:
A sum is infinite iff one term is infinite.
theorem
WithTop.sum_lt_top_iff
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
[LT α]
{s : Finset ι}
{f : ι → WithTop α}
:
A sum is finite iff all terms are finite.
theorem
WithTop.sum_lt_top
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
[LT α]
{s : Finset ι}
{f : ι → WithTop α}
(h : ∀ i ∈ s, f i ≠ ⊤)
:
(Finset.sum s fun (i : ι) => f i) < ⊤
A sum of finite terms is finite.
theorem
WithTop.prod_lt_top
{ι : Type u_1}
{α : Type u_2}
[CommMonoidWithZero α]
[NoZeroDivisors α]
[Nontrivial α]
[DecidableEq α]
[LT α]
{s : Finset ι}
{f : ι → WithTop α}
(h : ∀ i ∈ s, f i ≠ ⊤)
:
(Finset.prod s fun (i : ι) => f i) < ⊤
A product of finite terms is finite.
@[simp]
theorem
WithBot.coe_sum
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
(s : Finset ι)
(f : ι → α)
:
↑(Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => ↑(f i)
theorem
WithBot.sum_eq_bot_iff
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
{s : Finset ι}
{f : ι → WithBot α}
:
A sum is infinite iff one term is infinite.
theorem
WithBot.bot_lt_sum_iff
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
[LT α]
{s : Finset ι}
{f : ι → WithBot α}
:
A sum is finite iff all terms are finite.
theorem
WithBot.sum_lt_bot
{ι : Type u_1}
{α : Type u_2}
[AddCommMonoid α]
[LT α]
{s : Finset ι}
{f : ι → WithBot α}
(h : ∀ i ∈ s, f i ≠ ⊥)
:
⊥ < Finset.sum s fun (i : ι) => f i
A sum of finite terms is finite.
theorem
WithBot.prod_lt_bot
{ι : Type u_1}
{α : Type u_2}
[CommMonoidWithZero α]
[NoZeroDivisors α]
[Nontrivial α]
[DecidableEq α]
[LT α]
{s : Finset ι}
{f : ι → WithBot α}
(h : ∀ i ∈ s, f i ≠ ⊥)
:
⊥ < Finset.prod s fun (i : ι) => f i
A product of finite terms is finite.