Series laws Ⅱ: sums over finite sets

9 basic properties of sums over finite sets. The proofs of these are a good exercise to refresh the notions of functions, bijections, sets, sums and induction.

There is 1-1 correspondence between many of these properties and the 6 properties already shown for sums of the form [...]. Thus, proving many of them amounts to choosing a bijection that allows transitioning to one of the original properties.

1. [...]. If $X$ is empty, and $f:X\to \mathbb{R}$ is a function (i.e., $f$ is the empty function), we have

2. [...]. If $X$ consists of a single element, $X=\{x_0\}$, and $f:X\to \mathbb{R}$ is a function, we have

3. [...], part I. If $X$ is a finite set, $f:X\to \mathbb{R}$ is a function, and $g:Y\to X$ is a bijection, then

4. [...], part II. Let $n\le m$ be integers, and let $X$ be the set $X:=\{i\in \mathbb{Z}:n\le i\le m\}$. If $a_i$ is a real number assigned to each integer $i\in X$, then we have

5. [...]. Let $X$, $Y$ be disjoint finite sets ($X\cap Y=\mathrm{\varnothing }$), and $f:X\cup Y\to \mathbb{R}$ is a function. Then we have

6. [...], part I. Let $X$ be a finite set, and let $f:X\to \mathbb{R}$ and $g:X\to \mathbb{R}$ be functions. Then we have

7. [...], part II. Let $X$ be a finite set, and let $f:X\to \mathbb{R}$ be a function, and let $c$ be a real number. Then

8. [...]. Let $X$ be a finite set, and let $f:X\to \mathbb{R}$ and $g:X\to \mathbb{R}$ be functions such that $f(x)\le g(x)\text{ for all }x\in X$. Then

9. [...]. Let $X$ be a finite set, and let $f:X\to \mathbb{R}$ be a function, then