HepLean Documentation

Mathlib.Algebra.BigOperators.WithTop

Sums in WithTop #

This file proves results about finite sums over monoids extended by a bottom or top element.

source
@[simp]
theorem WithTop.coe_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (s : Finset ι) (f : ι → α) :
↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
source
@[simp]
theorem WithTop.sum_eq_top {ι : 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.

source
theorem WithTop.sum_ne_top {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {s : Finset ι} {f : ι → WithTop α} :
∑ i ∈ s, f i ≠ ⊤ ↔ ∀ i ∈ s, f i ≠ ⊤

A sum is finite iff all terms are finite.

source
@[simp]
theorem WithTop.sum_lt_top {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {s : Finset ι} {f : ι → WithTop α} [LT α] :
∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤

A sum is finite iff all terms are finite.

source
@[deprecated WithTop.sum_eq_top]
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 = ⊤

Alias of WithTop.sum_eq_top.

A sum is infinite iff one term is infinite.

source
@[deprecated WithTop.sum_lt_top]
theorem WithTop.sum_lt_top_iff {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {s : Finset ι} {f : ι → WithTop α} [LT α] :
∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤

Alias of WithTop.sum_lt_top.

A sum is finite iff all terms are finite.

source
theorem WithTop.prod_ne_top {ι : Type u_1} {α : Type u_2} [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] [DecidableEq α] {s : Finset ι} {f : ι → WithTop α} (h : ∀ i ∈ s, f i ≠ ⊤) :
∏ i ∈ s, f i ≠ ⊤

A product of finite terms is finite.

source
theorem WithTop.prod_lt_top {ι : Type u_1} {α : Type u_2} [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] [DecidableEq α] {s : Finset ι} {f : ι → WithTop α} [LT α] (h : ∀ i ∈ s, f i < ⊤) :
∏ i ∈ s, f i < ⊤

A product of finite terms is finite.

source
@[simp]
theorem WithBot.coe_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (s : Finset ι) (f : ι → α) :
↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
source
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.

source
theorem WithBot.bot_lt_sum_iff {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {s : Finset ι} {f : ι → WithBot α} [LT α] :
⊥ < ∑ i ∈ s, f i ↔ ∀ i ∈ s, ⊥ < f i

A sum is finite iff all terms are finite.

source
theorem WithBot.sum_lt_bot {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {s : Finset ι} {f : ι → WithBot α} [LT α] (h : ∀ i ∈ s, f i ≠ ⊥) :
⊥ < ∑ i ∈ s, f i

A sum of finite terms is finite.

source
theorem WithBot.prod_ne_bot {ι : Type u_1} {α : Type u_2} [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] [DecidableEq α] {s : Finset ι} {f : ι → WithBot α} (h : ∀ i ∈ s, f i ≠ ⊥) :
∏ i ∈ s, f i ≠ ⊥

A product of finite terms is finite.

source
theorem WithBot.bot_lt_prod {ι : Type u_1} {α : Type u_2} [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] [DecidableEq α] {s : Finset ι} {f : ι → WithBot α} [LT α] (h : ∀ i ∈ s, ⊥ < f i) :
⊥ < ∏ i ∈ s, f i

A product of finite terms is finite.

source
@[deprecated WithBot.bot_lt_prod]
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.