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 : ι → α) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

theorem WithTop.sum_eq_top_iff {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {s : Finset ι} {f : ι → WithTop α} : ∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, 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 α} : ∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, 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 : ∀ i ∈ s, f i ≠ ⊤) : ∑ i ∈ s, 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 ≠ ⊤) : ∏ i ∈ s, f i < ⊤

A product of finite terms is finite.

@[simp]

theorem WithBot.coe_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (s : Finset ι) (f : ι → α) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

theorem WithBot.sum_eq_bot_iff {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {s : Finset ι} {f : ι → WithBot α} : ∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, 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 α} : ⊥ < ∑ i ∈ s, f i ↔ ∀ i ∈ s, ⊥ < 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 : ∀ i ∈ s, f i ≠ ⊥) : ⊥ < ∑ i ∈ s, 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 ≠ ⊥) : ⊥ < ∏ i ∈ s, f i

A product of finite terms is finite.