Proof of Total Lengths of Covers by Open Intervals: the Set of Them and the Map of Their Infima

Proof of (i). Let $A\subseteq\mathbb{R}$. For sequences $(a_{m})$ and $(b_{m})$ in $\mathbb{R}$ with $a_{m}\le b_{m}$ for every $m\in\mathbb{N}$, $m\mapsto(a_{m},b_{m})$ is a sequence in $\mathcal{P}(\mathbb{R})$ (Intervals of the Real Line as Defined Set Symbols, Typed Terms and Values of Maps (iii)) and the union is that of this family, so the inclusion $A\subseteq\bigcup_{m\in\mathbb{N}}(a_{m},b_{m})$ says that every $x\in A$ lies in $(a_{m},b_{m})$ for some $m\in\mathbb{N}$, by Indexed Families of Sets and Their Union, Intersection and Product (ii); and $\sum_{m\in\mathbb{N}}(b_{m}-a_{m})$ lies in $[0,\infty]$. So $\mathcal{C}(A)$ is the class of all $t\in[0,\infty]$ satisfying the condition "there are such sequences with $t=\sum_{m\in\mathbb{N}}(b_{m}-a_{m})$". We show that this condition is expressed by a predicative formula whose parameters are $A$, $\mathbb{N}$, $\mathbb{R}$, $\mathbb{R}^{\mathbb{N}}$, the order $\le$, the operations $+$ and $\cdot$ and the elements $0$ and $1$ of $\mathbb{R}$, $\mathcal{P}(\mathbb{R})$, $[-\infty,\infty]$ and its order $\le$, $[0,\infty]$, $[0,\infty]^{\mathbb{N}}$, the sum $+$ on $[0,\infty]$, and the order and the addition of $\mathbb{N}_{0}$, and which quantifies over sets only, the sequences in it being elements of the set $\mathbb{R}^{\mathbb{N}}$ of The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii). The class variables for these parameters are chosen pairwise distinct whenever their values differ: in particular the order of $\mathbb{R}$ and the order of $[-\infty,\infty]$ are different variables, although Intervals of the Real Line as Defined Set Symbols, Typed Terms and Values of Maps (ii) and Sums of Sequences in [0,∞] as Typed Terms and as a Map (i) both write $L$ for theirs, and likewise $+$ of $\mathbb{R}$ and the sum $+$ on $[0,\infty]$. Then $\mathcal{C}(A)$ is a subset of $[0,\infty]$ given by set-builder notation as in Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices (iv), and its elements are exactly the sets $t$ satisfying the condition, as stated.

The sequences are values of set variables $a$ and $b$ of the formula, not fixed maps. Let $\gamma$ be the formula $a\in\mathbb{R}^{\mathbb{N}}\wedge b\in\mathbb{R}^{\mathbb{N}}\wedge\forall m\,(m\in\mathbb{N}\Rightarrow\exists u\,\exists v\,((m,u)\in a\wedge(m,v)\in b\wedge u\le v))$, a guard on $a$ and $b$, and $\gamma_{m}$ the guard $\gamma\wedge m\in\mathbb{N}$ on $a$, $b$ and $m$; they are predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). If $a$ is a map with domain $\mathbb{N}$ and $m\in\mathbb{N}$, then for every set $z$, $(m,z)\in a$ if and only if $z=a_{m}$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x), and likewise for $b$; so $\gamma$ holds exactly when $(a_{m})$ and $(b_{m})$ are sequences in $\mathbb{R}$ with $a_{m}\le b_{m}$ for every $m\in\mathbb{N}$. The formula $\gamma_{m}\wedge(m,z)\in a$ thus expresses $\gamma_{m}\wedge z=a_{m}$, and $a_{m}\in\mathbb{R}$, so $a_{m}$ is a term of type $\mathbb{R}$ under $\gamma_{m}$ by Terms and Typed Terms under a Guard (ii), and so is $b_{m}$.

The difference $b_{m}-a_{m}$ is the value of the subtraction of the ordered field $\mathbb{R}$ at the pair $(b_{m},a_{m})$: by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (iv) there is a predicative formula $\delta(u,v,z)$, with $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$ as parameters, that holds if and only if $u\in\mathbb{R}$, $v\in\mathbb{R}$ and $z=u-v$; hence $\gamma_{m}\wedge\exists u\,\exists v\,((m,u)\in b\wedge(m,v)\in a\wedge\delta(u,v,z))$, predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), expresses $\gamma_{m}\wedge z=b_{m}-a_{m}$, since under $\gamma_{m}$ the only such $u$ and $v$ are $b_{m}$ and $a_{m}$; and as $b_{m}-a_{m}\in[0,\infty]$, $b_{m}-a_{m}$ is a term of type $[0,\infty]$ under $\gamma_{m}$. Thus $b_{m}-a_{m}$ is an expression built from the defined set symbols $a_{m}$, $b_{m}$ and $u-v$, given by the formulas above, with no class abstraction, used properly and lying in $[0,\infty]$ for all $a$ and $b$ satisfying $\gamma$ and every $m\in\mathbb{N}$. So Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v), with $\mathbb{N}$ and $[0,\infty]$ for its $A$ and $B$, $a$ and $b$ for its $v_{1}$ and $v_{2}$, $\gamma$ for its $\gamma$, $m$ for its $u$ and $b_{m}-a_{m}$ for its $t(u,v_{1},v_{2})$, gives a predicative formula $\theta(h,a,b)$ such that, for all $a$ and $b$ satisfying $\gamma$, the only set $h$ with $\theta(h,a,b)$ is the map $m\mapsto b_{m}-a_{m}$ from $\mathbb{N}$ to $[0,\infty]$. Hence $\gamma\wedge\theta(h,a,b)$ expresses "$\gamma$ holds and $h$ is the map $m\mapsto b_{m}-a_{m}$", and this map is an element of $[0,\infty]^{\mathbb{N}}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i); so $m\mapsto b_{m}-a_{m}$ is a term of type $[0,\infty]^{\mathbb{N}}$ under $\gamma$, by Terms and Typed Terms under a Guard (ii).

By Sums of Sequences in [0,∞] as Typed Terms and as a Map (i), with $[-\infty,\infty]$, its order, $[0,\infty]$, the sum on $[0,\infty]$, $\mathbb{N}$, and the order and the addition of $\mathbb{N}_{0}$ as the values of its $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$, the sum $\sum_{m\in\mathbb{N}}(b_{m}-a_{m})$ is a term of type $[0,\infty]$ under $\gamma$; and by Intervals of the Real Line as Defined Set Symbols, Typed Terms and Values of Maps (ii), with $\mathbb{R}$ and its order as the values of its $Y$ and $L$, the interval $(a_{m},b_{m})$ is a term of type $\mathcal{P}(\mathbb{R})$ under $\gamma_{m}$. By Terms and Typed Terms under a Guard (iv), predicative formulas then express $\gamma\wedge t=\sum_{m\in\mathbb{N}}(b_{m}-a_{m})$ and $\gamma_{m}\wedge z=(a_{m},b_{m})$, for set variables $t$ and $z$ occurring in neither term; $x\in(a_{m},b_{m})$ is expressed under $\gamma_{m}$ by $\exists z\,(z=(a_{m},b_{m})\wedge x\in z)$ with the latter formula; and the condition is $\exists a\,\exists b$ applied to the conjunction of $\gamma$, $\forall x\,(x\in A\Rightarrow\exists m\,(m\in\mathbb{N}\wedge x\in(a_{m},b_{m})))$ and $t=\sum_{m\in\mathbb{N}}(b_{m}-a_{m})$, so expressed, which is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). This is the predicative formula claimed above, which proves (i).

Proof of (ii). Let $A\subseteq\mathbb{R}$. By (i), $\mathcal{C}(A)$ is a subset of $[0,\infty]$, hence of $[-\infty,\infty]$ (The Extended Real Line, Its Order, and [0,∞] (ii)); so it has an infimum in $[-\infty,\infty]$ by Order and Suprema in the Extended Real Line (iii), and $\inf\mathcal{C}(A)\in[0,\infty]$ by Order and Suprema in the Extended Real Line (ix). The elements of $\mathcal{P}(\mathbb{R})$ are exactly the subsets of $\mathbb{R}$ (The Union Set and the Power Set of a Set (ii)), and $\mathcal{C}(A)$ is the class given, with $A$ as its argument, by the predicative condition of the proof of (i), in which $A$ occurs only as a set and may be taken as a set variable. So Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima (iii), with $\mathcal{P}(\mathbb{R})$ for its $a$, $[-\infty,\infty]$ and $\le$ for its $p$ and $\preceq$ ($\le$ being a total order by Order and Suprema in the Extended Real Line (i), hence a partial order by Partial and Total Orders on a Set and the Associated Strict Relation (ii)), and $\mathcal{C}(A)$ for its $t(u)$, gives exactly one map $f:\mathcal{P}(\mathbb{R})\to[-\infty,\infty]$ with $f(A)=\inf\mathcal{C}(A)$ for every $A\in\mathcal{P}(\mathbb{R})$. Its values lie in $[0,\infty]$, so $f$ is a map into $[0,\infty]$ by Functions, Values of a Function, and Functions from One Class to Another (iii); and any map $\mathcal{P}(\mathbb{R})\to[0,\infty]$ with these values is also one into $[-\infty,\infty]$, hence equal to $f$. This proves (ii).