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}
{M : Type u_2}
[AddCommMonoid M]
(s : Finset ι)
(f : ι → M)
:
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 ≠ ⊤)
:
A product of finite terms is finite.
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 < ⊤)
:
A product of finite terms is finite.
@[simp]
theorem
WithBot.coe_sum
{ι : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
(s : Finset ι)
(f : ι → M)
:
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 ≠ ⊥)
:
A product of finite terms is finite.
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)
:
A product of finite terms is finite.