Toolkit for CA1c

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and Measurable Functions and the Lebesgue Integral: Notation: $<$ is the strict relation of the order $\le$ of $\mathbb{R}$, $-x$ and $x-y$ are the negative and the difference, $y^{-1}$ and $x/y$ (for $y\neq0$) the reciprocal and the quotient, and $|x|$ is the absolute value.

(i) $0\le1$ in $\mathbb{R}$.

(ii) If $x\in\mathbb{R}$ and $x\neq0$, then $0<x\cdot x$.

(iii) If $x\in\mathbb{R}$ and $x\cdot x\neq0$, then $x\neq0$.

(iv) For every element $y$ of the type $\mathrm{Real}$ of The Real Numbers as a Type (i), with $0$, $1$, $+$ and $\cdot$ as in The Real Numbers as a Type (ii), $1+y\cdot y\neq0$.

(v) If $a\in\mathbb{R}$ and $a\neq0$, then $|a|\in\mathbb{R}$, $0<|a|$, $|a|^{-1}\in\mathbb{R}$, $0<|a|^{-1}$ and

$$|a|^{-1}\cdot|a|=1 .$$

(vi) If $k,l\in\mathbb{R}$, $0<k$, $0<l$ and $x\in[0,\infty]$, the set of The Extended Real Line, Its Order, and [0,∞] (ii), then

$$k\,(l\,x)=(k\cdot l)\,x ,$$

where $k\cdot l$ is the product in $\mathbb{R}$ and the other three products are the product on $[0,\infty]$.

(vii) If $a,b\in\mathbb{R}$ and $T:\mathbb{R}\to\mathbb{R}$ is a map with $T(x)=ax+b$ for every $x\in\mathbb{R}$, then $T$ is continuous from $\mathbb{R}$ to $\mathbb{R}$, both carrying the distance $d_{\mathbb{R}}$.

(viii) If $a,b,u,v\in\mathbb{R}$ and $T:\mathbb{R}\to\mathbb{R}$ is a map with $T(x)=ax+b$ for every $x\in\mathbb{R}$, then, for the half-open intervals and the preimage $T^{-1}[\cdot]$: if $0<a$, then

$$T^{-1}[(u,v]]=\Bigl(\frac{u-b}{a},\frac{v-b}{a}\Bigr] ;$$

and if $a<0$, then

$$T^{-1}[(u,v]]=\Bigl[\frac{v-b}{a},\frac{u-b}{a}\Bigr) .$$

(ix) If $n\in\mathbb{N}$ and $x,y\in\mathbb{R}^{n}$, the space of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (i), then $x+y=y+x$ for the sum of $\mathbb{R}^{n}$.

(x) For every $n\in\mathbb{N}$, the set $\mathcal{M}_{n}(\mathbb{R})$ of square real matrices of Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i) equals the set $\mathcal{M}_{n}(\mathbb{R})$ of square real matrices of Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i).

(xi) If $(X,\mathcal{F},\mu)$ is a measure space and $h\in\mathcal{M}^{+}(X,\mathcal{F})$, then the measure $h\mu$ with density $h$ with respect to $\mu$ is a map $h\mu:\mathcal{F}\to[0,\infty]$ with

$$(h\mu)(A)=\int_{A}h\,d\mu\qquad(A\in\mathcal{F}).$$