Suprema and Finite Sums in [0,∞]

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $[0,\infty]$ and the order $\le$ be as in The Extended Real Line, Its Order, and [0,∞] (ii) and The Extended Real Line, Its Order, and [0,∞] (iii), the sum $+$ and the product $\cdot$ on $[0,\infty]$ as in Addition and Multiplication on [0,∞] (i) and Addition and Multiplication on [0,∞] (ii), and suprema and $\sup_{n}$ as in Order and Suprema in the Extended Real Line (iii). Let $c\in[0,\infty]$ and let $X$ be a nonempty subset of $[0,\infty]$.

(i) $\sup\{x+c:x\in X\}=\sup X+c$.

(ii) $\sup\{cx:x\in X\}=c\sup X$.

(iii) If $(u_{n})$ and $(v_{n})$ are sequences in $[0,\infty]$ with $u_{n}\le u_{n+1}$ and $v_{n}\le v_{n+1}$ for every $n\in\mathbb{N}$, then $\sup_{n}(u_{n}+v_{n})=\sup_{n}u_{n}+\sup_{n}v_{n}$.

Let $A$ be a finite set. Sums over $A$ of maps into $[0,\infty]$ are as in Sums and Products over a Finite Set and over an Interval (i), Sums and Products over a Finite Set and over an Interval (ii), Sums and Products over a Finite Set and over an Interval (iii) and Sums and Products over a Finite Set and over an Interval (v), for the operation $+$, which is associative and commutative with neutral element $0$ by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i).

(iv) If $f,g:A\to[0,\infty]$ satisfy $f(y)\le g(y)$ for every $y\in A$, then $\sum_{y\in A}f(y)\le\sum_{y\in A}g(y)$.

(v) If $f:A\to[0,\infty]$ and $B\subseteq A$, then $\sum_{y\in B}f(y)\le\sum_{y\in A}f(y)$.

(vi) If $f:A\to[0,\infty]$, then $c\sum_{y\in A}f(y)=\sum_{y\in A}cf(y)$.

(vii) $\sum_{y\in A}0=0$.

(viii) If $w:\mathbb{N}\times A\to[0,\infty]$ satisfies $w(n,y)\le w(n+1,y)$ for all $n\in\mathbb{N}$ and $y\in A$, then $\sum_{y\in A}\sup_{n}w(n,y)=\sup_{n}\sum_{y\in A}w(n,y)$.