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

A sum is finite iff all terms are finite.

source
theorem WithTop.prod_ne_top {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀} (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} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀} [LT M₀] (h : ∀ i ∈ s, f i < ⊤) :
∏ i ∈ s, f i < ⊤

A product of finite terms is finite.

source
theorem WithTop.prod_eq_top {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀} {i : ι} (hi : i ∈ s) (hi' : f i = ⊤) (h : ∀ j ∈ s, f j ≠ 0) :
∏ j ∈ s, f j = ⊤
source
theorem WithTop.prod_eq_top_ne_zero {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀} {i : ι} (hi : i ∈ s) (h : ∏ j ∈ s, f j = ⊤) :
f i ≠ 0
source
theorem WithTop.prod_eq_top_ex_top {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀} (h : ∏ j ∈ s, f j = ⊤) :
∃ i ∈ s, f i = ⊤
source
theorem WithTop.prod_eq_top_iff {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀} :
∏ j ∈ s, f j = ⊤ ↔ (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0

A product is infinite iff each factor is nonzero and some factor is infinite

source
@[simp]
theorem WithBot.coe_sum {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (s : Finset ι) (f : ι → M) :
↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
source
theorem WithBot.sum_eq_bot_iff {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {s : Finset ι} {f : ι → WithBot M} :
∑ 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} {M : Type u_2} [AddCommMonoid M] {s : Finset ι} {f : ι → WithBot M} [LT M] :
⊥ < ∑ 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} {M : Type u_2} [AddCommMonoid M] {s : Finset ι} {f : ι → WithBot M} [LT M] (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} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ι → WithBot M₀} (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} {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] [DecidableEq M₀] {s : Finset ι} {f : ι → WithBot M₀} [LT M₀] (h : ∀ i ∈ s, ⊥ < f i) :
⊥ < ∏ i ∈ s, f i

A product of finite terms is finite.