Documentation

Mathlib.Algebra.BigOperators.WithTop

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 : ια) :
(is, f i) = is, (f i)
theorem WithTop.sum_eq_top_iff {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {s : Finset ι} {f : ιWithTop α} :
is, f i = is, f i =

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 α} :
is, f i < is, f i <

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 : is, f i ) :
is, 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 : is, f i ) :
is, f i <

A product of finite terms is finite.

@[simp]
theorem WithBot.coe_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (s : Finset ι) (f : ια) :
(is, f i) = is, (f i)
theorem WithBot.sum_eq_bot_iff {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {s : Finset ι} {f : ιWithBot α} :
is, f i = is, f i =

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 α} :
< is, f i is, < f i

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 : is, f i ) :
< is, 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 : is, f i ) :
< is, f i

A product of finite terms is finite.