Proof of Toolkit for CA1c

Routine facts about real numbers, maps and the type $\mathrm{Real}$ are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, Arithmetic and Order Rules in the Real Numbers, Stated for ℝ). Recall that $s<t$ means $s\le t$ and $s\neq t$ (Partial and Total Orders on a Set and the Associated Strict Relation (iii)).

Proof of (i). By Rules of Arithmetic and Order in an Ordered Field (vii), $0<1$, and in particular $0\le1$.

Proof of (ii). Let $x\in\mathbb{R}$ with $x\neq0$. Then $0\le x\cdot x$ by Rules of Arithmetic and Order in an Ordered Field (vii), and $x\cdot x\neq0$ by Rules of Arithmetic and Order in an Ordered Field (iii), applied to the two nonzero factors $x$ and $x$. Hence $0<x\cdot x$.

Proof of (iii). Let $x\in\mathbb{R}$. If $x=0$, then $x\cdot x=0\cdot0=0$. So $x\cdot x\neq0$ forces $x\neq0$.

Proof of (iv). Let $y$ be an element of $\mathrm{Real}$. Two elements of $\mathrm{Real}$ are equal exactly when their sets are (The Real Numbers as a Type (i)), and $0$, $1$, $+$ and $\cdot$ of $\mathrm{Real}$ are those of $\mathbb{R}$ (The Real Numbers as a Type (ii)); so it suffices to show $1+y\cdot y\neq0$ in $\mathbb{R}$ for the real number $y$. In $\mathbb{R}$, $0\le y\cdot y$ and $0<1$ by Rules of Arithmetic and Order in an Ordered Field (vii), and adding $y\cdot y$ to both sides of $0<1$ preserves the strict inequality (Rules of Arithmetic and Order in an Ordered Field (iv)):

$$y\cdot y<1+y\cdot y .$$

Suppose $1+y\cdot y=0$. Then $y\cdot y<0$, that is, $y\cdot y\le0$ and $y\cdot y\neq0$ (Partial and Total Orders on a Set and the Associated Strict Relation (iii)). Together with $0\le y\cdot y$, antisymmetry of $\le$ (Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (viii)) gives $y\cdot y=0$, a contradiction. Hence $1+y\cdot y\neq0$.

Proof of (v). Let $a\in\mathbb{R}$ with $a\neq0$. By Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (ix), $|a|\in\mathbb{R}$ and $0\le|a|$; and $|a|\neq0$, since $|a|=0$ only for $a=0$ (Rules of Arithmetic and Order in an Ordered Field (x)). Hence $0<|a|$. As $|a|\neq0$, its reciprocal $|a|^{-1}\in\mathbb{R}$ is defined and satisfies $|a|\cdot|a|^{-1}=1$ (Negatives, Differences, Reciprocals and Quotients (ii), The Real Numbers as a Type (vii)), so $|a|^{-1}\cdot|a|=1$ by commutativity of the product. Finally $0<|a|^{-1}$ by Rules of Arithmetic and Order in an Ordered Field (viii).

Proof of (vi). Let $k,l\in\mathbb{R}$ with $0<k$ and $0<l$, and let $x\in[0,\infty]$. Then $k,l\in[0,\infty]$ by The Extended Real Line, Its Order, and [0,∞] (ii), and the product of $k$ and $l$ in $[0,\infty]$ is their product $k\cdot l$ in $\mathbb{R}$, as both are real (Addition and Multiplication on [0,∞] (ii)). The product on $[0,\infty]$ is associative (Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (ii)), so $k\,(l\,x)$ is the product in $[0,\infty]$ of $k\,l$ and $x$, that is, $(k\cdot l)\,x$.

Proof of (vii). Let $a,b\in\mathbb{R}$ and $T$ be as stated. The real line $(\mathbb{R},d_{\mathbb{R}})$ is a metric space by The Absolute Value Metric on the Real Numbers (i), and $d_{\mathbb{R}}(s,t)=|s-t|$ for $s,t\in\mathbb{R}$ (The Distance on the Real Numbers Is a Map with Values the Absolute Differences (ii)). For $x,x'\in\mathbb{R}$, using $|s\cdot t|=|s|\cdot|t|$ (Rules of Arithmetic and Order in an Ordered Field (x), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iv)),

$$d_{\mathbb{R}}\bigl(T(x),T(x')\bigr)=\bigl|(ax+b)-(ax'+b)\bigr|=|a\,(x-x')|=|a|\cdot d_{\mathbb{R}}(x,x').$$

As $|a|$ is a real number with $0\le|a|$ (Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (ix)), $T$ is Lipschitz with constant $|a|$, and therefore continuous by A Lipschitz Map is Uniformly Continuous and Continuous (ii).

Proof of (viii). Let $a,b,u,v\in\mathbb{R}$ and $T$ be as stated. Both sides of each identity are subsets of $\mathbb{R}$, and a real number $x$ lies in $T^{-1}[(u,v]]$ exactly when $T(x)\in(u,v]$ (The Image and the Preimage of a Class under a Class (ii), Intervals of the Real Line (ii)), that is, when $u<ax+b\le v$. Adding $-b$, resp. $b$, to all sides (Rules of Arithmetic and Order in an Ordered Field (iv)), this holds if and only if

$$u-b<ax\le v-b .$$

Put $p=(u-b)/a$ and $q=(v-b)/a$. A quotient $s/a$ is the real number whose product with $a$ is $s$ (Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (ii)), so

$$p\cdot a=u-b,\qquad q\cdot a=v-b .$$

We compare $x$ with $p$ and $q$ by multiplying with a positive factor, which preserves and reflects both $\le$ and $<$ (Rules of Arithmetic and Order in an Ordered Field (vi)).

Case $0<a$. Multiplying by $a$, we get $p<x$ if and only if $p\cdot a<x\cdot a$, that is, $u-b<ax$; and $x\le q$ if and only if $x\cdot a\le q\cdot a$, that is, $ax\le v-b$. So the condition is $p<x\le q$, that is, $x\in\bigl((u-b)/a,(v-b)/a\bigr]$.

Case $a<0$. Put $c=-a$; then $0<c$ (Rules of Arithmetic and Order in an Ordered Field (v)), and $y\cdot c=-(y\cdot a)$ for every $y\in\mathbb{R}$ (Rules of Arithmetic and Order in an Ordered Field (ii)); in particular

$$x\cdot c=-(ax),\qquad p\cdot c=-(u-b),\qquad q\cdot c=-(v-b).$$

Negation reverses $\le$, and hence also $<$ (Rules of Arithmetic and Order in an Ordered Field (v)). So $u-b<ax$ if and only if $x\cdot c<p\cdot c$, that is, multiplying by $c$, if and only if $x<p$; and $ax\le v-b$ if and only if $q\cdot c\le x\cdot c$, that is, $q\le x$. So the condition is $q\le x<p$, that is, $x\in\bigl[(v-b)/a,(u-b)/a\bigr)$.

In either case the two sides have the same elements, so they are equal.

Proof of (ix). Let $n\in\mathbb{N}$ and $x,y\in\mathbb{R}^{n}$. For every $k\in[n]$,

$$(x+y)_{k}=x_{k}+y_{k}=y_{k}+x_{k}=(y+x)_{k}$$

by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iv) and commutativity of the sum of $\mathbb{R}$. As $x+y$ and $y+x$ lie in $\mathbb{R}^{n}$, they are equal by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii).

Proof of (x). Let $n\in\mathbb{N}$. Both Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i) and Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i) define $\mathcal{M}_{n}(\mathbb{R})$ as $\mathcal{M}_{n\times n}(\mathbb{R})$, the set $\mathbb{R}^{[n]\times[n]}$ of all maps $[n]\times[n]\to\mathbb{R}$, from the same segment $[n]$ and the same set $\mathbb{R}$. So the two sets are the same set.

Proof of (xi). Let $(X,\mathcal{F},\mu)$ be a measure space and $h\in\mathcal{M}^{+}(X,\mathcal{F})$. (The earlier versions of $\sigma$-algebras, of measure spaces, of $\mathcal{M}^{+}(X,\mathcal{F})$ and of its integral, in which the results used below are stated, define the same objects: The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (i), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (iii), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (v).) For each $A\in\mathcal{F}$, the map $h\mathbf{1}_{A}$ lies in $\mathcal{M}^{+}(X,\mathcal{F})$ and the integral of $h$ over $A$ (Integrals of Functions over a Measurable Subset (ii)) is

$$\int_{A}h\,d\mu=\int_{X}h\mathbf{1}_{A}\,d\mu$$

by Integrals over Measurable Subsets (i). (So $A\mapsto\int_{A}h\,d\mu$ is a map $\mathcal{F}\to[0,\infty]$: the map $A\mapsto h\mathbf{1}_{A}$ from $\mathcal{F}$ to $\mathcal{M}^{+}(X,\mathcal{F})$, Maps and Relations Given by Formulas (i), followed by the integral on $\mathcal{M}^{+}(X,\mathcal{F})$.) By Measure with a Density (i), $h\mu$ is the function on $\mathcal{F}$ with these values; hence $h\mu:\mathcal{F}\to[0,\infty]$ and $(h\mu)(A)=\int_{A}h\,d\mu$ for every $A\in\mathcal{F}$.