WithTop.sum_lt_top_iff
theorem WithTop.sum_lt_top_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LT α] {s : Finset ι} {f : ι → WithTop α},
(s.sum fun i => f i) < ⊤ ↔ ∀ i ∈ s, f i < ⊤
The theorem `WithTop.sum_lt_top_iff` states that for any type `α` equipped with a commutative monoidal addition and a less-than relation, and any finitely indexed set of elements of `α` with the top element (`WithTop α`), the sum of these elements is less than the top element if and only if each individual element is less than the top element. Here, the top element is a designated maximum or "infinity" value added to the type `α` by the `WithTop` constructor. In other words, the sum of a set of possibly infinite values is finite if and only if all the elements in the set are finite.
More concisely: For any commutative monoid with a least element `top` and a set of elements in a type `α`, the sum of those elements is less than `top` if and only if each element is less than `top`.
|
WithTop.sum_eq_top_iff
theorem WithTop.sum_eq_top_iff :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] {s : Finset ι} {f : ι → WithTop α},
(s.sum fun i => f i) = ⊤ ↔ ∃ i ∈ s, f i = ⊤
This theorem states that for any type `ι`, any type `α` equipped with an addition operation (`AddCommMonoid α`), any finite set `s` of elements of type `ι`, and any function `f` from `ι` to the type `α` with an additional `⊤` (which represents infinity in `WithTop α`), the sum of the function `f` applied to each element in the set `s` is infinite (`⊤`) if and only if there exists an element `i` in the set `s` such that the function `f` applied to `i` is infinite (`⊤`).
More concisely: For any type `ι`, any AddCommMonoid `α`, finite set `s ⊆ ι`, and function `f : ι → α ∪ {⊤}`, the sum of `f s` is infinite if and only if there exists an element `i ∈ s` such that `f i = ⊤`.
|
WithTop.prod_lt_top
theorem WithTop.prod_lt_top :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : NoZeroDivisors α] [inst_2 : Nontrivial α]
[inst_3 : DecidableEq α] [inst_4 : LT α] {s : Finset ι} {f : ι → WithTop α},
(∀ i ∈ s, f i ≠ ⊤) → (s.prod fun i => f i) < ⊤
This theorem states that for any type `ι` and `α`, given that `α` is a commutative monoid with zero, has no zero divisors, is nontrivial, and has decidable equality as well as a less than operation, for any finite set `s` of type `ι` and a function `f` mapping from `ι` to optionally `α` (i.e., `α` topped with an extra element `⊤`), if all elements in `s` mapped by `f` are not `⊤`, then the product of these elements (each obtained by applying `f` to each element in `s`) is less than `⊤`. In essence, the product of finite terms from a set, under a specific function that maps to a type with a special top element, is also finite (not equal to the top element).
More concisely: For any commutative monoid `α` without zero divisors, decidable equality and ordering, and type `ι`, if `f : ι → option α` maps each element in a finite set `s μ` to a non-top element, then the product of `f s` is defined and strictly less than the top element.
|
WithTop.sum_lt_top
theorem WithTop.sum_lt_top :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LT α] {s : Finset ι} {f : ι → WithTop α},
(∀ i ∈ s, f i ≠ ⊤) → (s.sum fun i => f i) < ⊤
This theorem states that for any given index type `ι`, any type `α` with an additive commutative monoid structure and a less-than relation, a finite set `s` of indices, and a function `f` from indices to `α` with an additional top element (`WithTop α`), if for every index in the set `s`, the function `f` does not map that index to the top element, then the sum over `s` of `f` is strictly less than the top element. In terms of mathematics, given a finite index set $s$ and a function $f : ι → α \cup \{∞\}$ such that $f(i) < ∞$ for all $i \in s$, we have $\sum_{i \in s} f(i) < ∞$.
More concisely: Given a finite index set $s$ and a function $f : ι → α \cup \{∞\}$ with $f(i) < ∞$ for all $i \in s$, the sum $\sum\_{i \in s} f(i)$ is strictly less than the top element $\infty$ in $\alpha$.
|