ThmDex – An index of mathematical definitions, results, and conjectures.
Isotonicity of unsigned basic real series
Formulation 0
Let $x, y : \mathbb{N} \to [0, \infty)$ each be an D4686: Unsigned real sequence such that
(i) \begin{equation} x \leq y \end{equation}
Then \begin{equation} \sum_{n \in \mathbb{N}} x_n \leq \sum_{n \in \mathbb{N}} y_n \end{equation}
Formulation 1
Let $x_0, y_0, x_1, y_1, x_2, y_2, \ldots \in [0, \infty)$ each be an D4767: Unsigned real number such that
(i) \begin{equation} \forall \, n \in \mathbb{N} : x_n \leq y_n \end{equation}
Then \begin{equation} \sum_{n \in \mathbb{N}} x_n \leq \sum_{n \in \mathbb{N}} y_n \end{equation}
Proofs
Proof 0
Let $x, y : \mathbb{N} \to [0, \infty)$ each be an D4686: Unsigned real sequence such that
(i) \begin{equation} x \leq y \end{equation}
This result is a corollary to R2933: Isotonicity of countably infinite real summation. $\square$