Proof of Closed Boxes in $\mathbb{R}^n$ Are Compact

Each result cited is universally quantified over the data in its own statement. No choice principle is used: the boxes below are defined by recursion from maps given by formulas, and every other object is obtained from an existential statement or defined by a formula.

Let $n$, $d_{E}$, $a$, $b$ and $Q$ be as in the statement. By $\mathbb{R}^n$ with the Euclidean Distance Is a Complete Metric Space with Coordinatewise Convergence §metric, $d_{E}$ is a metric, so it satisfies Metric Space §symmetric; $\mathcal{T}_{d_{E}}$ is the topology of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §topology, and $\mathcal{T}_{Q}$ is the subspace topology on $Q$. By Compact Topological Space and Compact Subset §compact-subset and Compact Topological Space and Compact Subset §compact we must show: for every subset $\mathcal{U}$ of $\mathcal{T}_{Q}$ with $Q\subseteq\bigcup\mathcal{U}$ there is a finite subset $\mathcal{V}$ of $\mathcal{U}$ with $Q\subseteq\bigcup\mathcal{V}$. Fix such a $\mathcal{U}$.

Small sets. Call a subset $S$ of $Q$ small if there is a finite subset $\mathcal{V}$ of $\mathcal{U}$ with $S\subseteq\bigcup\mathcal{V}$. This is a predicative formula in $S$ with parameter $\mathcal{U}$ (it quantifies over sets only: subsets of $\mathcal{U}$, natural numbers and maps), so it may be used to form sets by Sets and Maps: Ordinary Notation §set-builder. We must show that $Q$ is small; suppose, for a contradiction, that $Q$ is not small.

(F1) If $S_{1},S_{2}\subseteq Q$ are small, so is $S_{1}\cup S_{2}$: if $\mathcal{V}_{1},\mathcal{V}_{2}$ are finite subsets of $\mathcal{U}$ with $S_{i}\subseteq\bigcup\mathcal{V}_{i}$, then $\mathcal{V}_{1}\cup\mathcal{V}_{2}$ is a finite subset of $\mathcal{U}$ by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §union, and $S_{1}\cup S_{2}\subseteq\bigcup(\mathcal{V}_{1}\cup\mathcal{V}_{2})$.

Boxes. Points of $\mathbb{R}^{n}$ are maps $[n]\to\mathbb{R}$ with components as in Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership, and two points are equal when their components agree, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §equality. Let

$$D=\{(\alpha,\beta)\in\mathbb{R}^{n}\times\mathbb{R}^{n}:a_{k}\le\alpha_{k}\le\beta_{k}\le b_{k}\text{ for every }k\in[n]\},$$

and for $p=(\alpha,\beta)\in D$ let $Q(p)=\{x\in\mathbb{R}^{n}:\alpha_{k}\le x_{k}\le\beta_{k}\text{ for every }k\in[n]\}$, a subset of $Q$ (the conditions defining $D$ and $Q(p)$ being predicative 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 §value-substitution); note $(a,b)\in D$ and $Q((a,b))=Q$. For $p=(\alpha,\beta)$ and $p'=(\alpha',\beta')$ in $D$ write $p'\sqsubseteq p$ if $\alpha_{k}\le\alpha'_{k}$ and $\beta'_{k}\le\beta_{k}$ for every $k\in[n]$; then $Q(p')\subseteq Q(p)$, and $\sqsubseteq$ is transitive. For $p=(\alpha,\beta)\in D$ and $k\in[n]$ write $w_{k}(p)=\beta_{k}-\alpha_{k}\ge0$ for the $k$-th side length, a real number by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §negative.

Halving one side. Let $j\in[n]$ and $p=(\alpha,\beta)\in D$, and let $c=(\alpha_{j}+\beta_{j})/2$, a real number by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §halves, so $\alpha_{j}\le c\le\beta_{j}$. Let $\beta'\in\mathbb{R}^{n}$ have components $\beta'_{j}=c$ and $\beta'_{k}=\beta_{k}$ for $k\neq j$, and $\alpha'\in\mathbb{R}^{n}$ components $\alpha'_{j}=c$ and $\alpha'_{k}=\alpha_{k}$ for $k\neq j$ (maps on $[n]$ given by Sets and Maps: Ordinary Notation §maps, their conditions being predicative 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 §value-substitution). Put $\lambda_{j}(p)=(\alpha,\beta')$ and $\rho_{j}(p)=(\alpha',\beta)$. Both lie in $D$, both satisfy $q\sqsubseteq p$, and for $q\in\{\lambda_{j}(p),\rho_{j}(p)\}$,

$$w_{j}(q)=\tfrac{1}{2}w_{j}(p),\qquad w_{k}(q)=w_{k}(p)\text{ for }k\in[n],\ k\neq j,$$

since $c-\alpha_{j}=\beta_{j}-c=(\beta_{j}-\alpha_{j})/2$. Moreover $Q(p)=Q(\lambda_{j}(p))\cup Q(\rho_{j}(p))$: the inclusion $\supseteq$ holds because both are $\sqsubseteq p$, and for $x\in Q(p)$ either $x_{j}\le c$, and then $x\in Q(\lambda_{j}(p))$, or $c<x_{j}$, and then $x\in Q(\rho_{j}(p))$.

Let $\varphi:[n]\times D\to D$ be the set

$$\varphi=\{((j,p),q)\in([n]\times D)\times D:\ (Q(\lambda_{j}(p))\text{ is not small and }q=\lambda_{j}(p))\text{ or }(Q(\lambda_{j}(p))\text{ is small and }q=\rho_{j}(p))\},$$

formed by Sets and Maps: Ordinary Notation §set-builder; exactly one of the two cases holds for each $(j,p)$, so $\varphi$ is a map $[n]\times D\to D$ by Functions, Values of a Function, and Functions from One Class to Another §map. Write $\varphi_{j}(p)=\varphi(j,p)$; thus $\varphi_{j}(p)$ is the left half $\lambda_{j}(p)$ if that is not small, and the right half $\rho_{j}(p)$ otherwise.

(F2) If $Q(p)$ is not small, then $Q(\varphi_{j}(p))$ is not small. If $Q(\lambda_{j}(p))$ is not small, $\varphi_{j}(p)=\lambda_{j}(p)$. Otherwise $Q(\lambda_{j}(p))$ is small and $\varphi_{j}(p)=\rho_{j}(p)$; were $Q(\rho_{j}(p))$ small too, $Q(p)=Q(\lambda_{j}(p))\cup Q(\rho_{j}(p))$ would be small by (F1).

One round: halving every side. Let $g:\mathbb{N}\times D\to D$ be the map with $g(k,u)=\varphi_{k}(u)$ for $k\in[n]$ and $g(k,u)=u$ for $k\in\mathbb{N}$ with $n<k$, a set by Sets and Maps: Ordinary Notation §set-builder and a map since exactly one case applies to each $(k,u)$. For $p\in D$, by Recursion on the Natural Numbers Starting at One §recursion (with the set $D$, the element $p$ and the map $g$) there is exactly one map $h_{p}:\mathbb{N}\to D$ with $h_{p}(1)=p$ and $h_{p}(k+1)=g(k,h_{p}(k))$ for every $k\in\mathbb{N}$. Let $\Phi:D\to D$ be the set of pairs $(p,q)\in D\times D$ such that $q=h(n+1)$ for some map $h:\mathbb{N}\to D$ with $h(1)=p$ and $h(k+1)=g(k,h(k))$ for every $k\in\mathbb{N}$; it is formed by Sets and Maps: Ordinary Notation §set-builder (the formula quantifies over the set $D^{\mathbb{N}}$ only), and it is a map with $\Phi(p)=h_{p}(n+1)$ by the existence and uniqueness of $h_{p}$.

(F3) Let $p=(\alpha,\beta)\in D$. For every $k\in[n+1]$: $h_{p}(k)\sqsubseteq p$; $Q(h_{p}(k))$ is not small if $Q(p)$ is not small; and for $i\in[n]$, $w_{i}(h_{p}(k))=\frac{1}{2}w_{i}(p)$ if $i<k$ and $w_{i}(h_{p}(k))=w_{i}(p)$ if $k\le i$. By induction on $k$, The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction, applied to the class $\{k\in\mathbb{N}:k\le n+1\Rightarrow P(k)\}$, where $P(k)$ is the claim just stated for $k$; this class is formed by a predicative formula with set parameters only (among them $p$, $h_{p}$, $n$ and $\mathcal{U}$). For $k=1$, $h_{p}(1)=p$ and there is no $i\in[n]$ with $i<1$. Let $k\in[n]$ and suppose the claim for $k$. Then $h_{p}(k+1)=g(k,h_{p}(k))=\varphi_{k}(h_{p}(k))$, which is $\lambda_{k}(h_{p}(k))$ or $\rho_{k}(h_{p}(k))$. Hence $h_{p}(k+1)\sqsubseteq h_{p}(k)\sqsubseteq p$; non-smallness passes on by (F2); and for $i\in[n]$: if $i<k$, then $i\neq k$ and $w_{i}(h_{p}(k+1))=w_{i}(h_{p}(k))=\frac{1}{2}w_{i}(p)$; if $i=k$, then $w_{k}(h_{p}(k+1))=\frac{1}{2}w_{k}(h_{p}(k))=\frac{1}{2}w_{k}(p)$; if $k+1\le i$, then $i\neq k$ and $w_{i}(h_{p}(k+1))=w_{i}(h_{p}(k))=w_{i}(p)$. Since $i<k+1$ exactly when $i<k$ or $i=k$, this is the claim for $k+1$.

Taking $k=n+1$, every $i\in[n]$ satisfies $i<n+1$, so for every $p\in D$: $\Phi(p)\sqsubseteq p$, $w_{i}(\Phi(p))=\frac{1}{2}w_{i}(p)$ for every $i\in[n]$, and $Q(\Phi(p))$ is not small if $Q(p)$ is not small.

The nested boxes. By Recursion on the Natural Numbers Starting at One §recursion (with the set $D$, the element $(a,b)$ and the map $(m,u)\mapsto\Phi(u)$ on $\mathbb{N}\times D$, given by Sets and Maps: Ordinary Notation §maps and 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 §value-substitution) there is a map $F:\mathbb{N}\to D$ with $F(1)=(a,b)$ and $F(m+1)=\Phi(F(m))$ for every $m\in\mathbb{N}$. Write $F(m)=(\alpha^{(m)},\beta^{(m)})$. By induction on $m$, The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction, applied to the class of those $m\in\mathbb{N}$ for which (N1)--(N3) below hold for every $k\in[n]$, formed by a predicative formula with set parameters only (among them $F$, $a$, $b$, $n$ and $\mathcal{U}$), and using the last paragraph, for every $m\in\mathbb{N}$ and $k\in[n]$: (N1) $Q(F(m))$ is not small (for $m=1$ this is the assumption on $Q$); (N2) $\beta^{(m)}_{k}-\alpha^{(m)}_{k}=(b_{k}-a_{k})(1/2)^{m-1}$ (exponents lie in $\mathbb{N}_{0}$, $m-1$ being the difference in $\mathbb{N}_{0}$ by Commutative Rings, Fields and Ordered Fields: Standard Notation §numerals, and $(1/2)^{0}=1$ by Commutative Rings, Fields and Ordered Fields: Standard Notation §rings and Powers with Exponents in the Natural Numbers with Zero §zero; $1/2$ and its powers lie in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §two, Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §quotient and Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §powers); (N3) $F(m+1)\sqsubseteq F(m)$, that is $\alpha^{(m)}_{k}\le\alpha^{(m+1)}_{k}$ and $\beta^{(m+1)}_{k}\le\beta^{(m)}_{k}$. By (N3), for each $k\in[n]$ the sequence $m\mapsto\alpha^{(m)}_{k}$ is nondecreasing and $m\mapsto\beta^{(m)}_{k}$ is nonincreasing, so by Monotone Sequences and Subsequences: Comparison of All Terms, Growth of the Indices, and Subsequences of Subsequences §monotone, $\alpha^{(m)}_{k}\le\alpha^{(m')}_{k}$ and $\beta^{(m')}_{k}\le\beta^{(m)}_{k}$ whenever $m\le m'$.

The limit point. Let $k\in[n]$. For all $m,m'\in\mathbb{N}$, $\alpha^{(m)}_{k}\le\beta^{(m')}_{k}$: if $m\le m'$, then $\alpha^{(m)}_{k}\le\alpha^{(m')}_{k}\le\beta^{(m')}_{k}$; if $m'<m$, then $\alpha^{(m)}_{k}\le\beta^{(m)}_{k}\le\beta^{(m')}_{k}$. So the nonempty set $A_{k}=\{\alpha^{(m)}_{k}:m\in\mathbb{N}\}\subseteq\mathbb{R}$ is bounded above, and it has a supremum $s_{k}=\sup A_{k}$ by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §supremum, unique as the least upper bound. Being an upper bound of $A_{k}$, $s_{k}\ge\alpha^{(m)}_{k}$; being the least one, $s_{k}\le\beta^{(m)}_{k}$, for every $m\in\mathbb{N}$. Let $s\in\mathbb{R}^{n}$ be the map $k\mapsto s_{k}$ on $[n]$, given by Sets and Maps: Ordinary Notation §maps and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership. Then $s\in Q(F(m))$ for every $m\in\mathbb{N}$; in particular $s\in Q(F(1))=Q$.

The contradiction. Since $s\in Q\subseteq\bigcup\mathcal{U}$, there is $W\in\mathcal{U}$ with $s\in W$. As $W\in\mathcal{T}_{Q}$, $W=Q\cap U$ for some $U\in\mathcal{T}_{d_{E}}$ by Subspace Topology §subspace-topology, and $U$ is open in $(\mathbb{R}^{n},d_{E})$ by Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §topology. As $s\in U$, there is a real $r>0$ with $B_{d_{E}}(s,r)\subseteq U$, by Open Subset of a Metric Space §open.

Let $w=\lVert b-a\rVert\ge0$, the Euclidean norm of $b-a$. For $k\in[n]$, $(b-a)_{k}=b_{k}-a_{k}\ge0$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations, so $b_{k}-a_{k}=|(b-a)_{k}|\le w$ by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §coordinate. Now, in this order: $r$ is fixed above; put $\varepsilon=r/(2(nw+1))>0$, a real number by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §naturals, Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §two and Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §quotient; by Completeness of the Real Numbers for Sequences: Monotone Convergence, the Bolzano-Weierstrass Theorem and Cauchy Sequences §geometric with ratio $1/2$, $(1/2)^{m}\to0$, so by Convergent Sequences of Real Numbers §converges there is $N\in\mathbb{N}$ with $(1/2)^{N}=|(1/2)^{N}-0|<\varepsilon$. Then $(1/2)^{N-1}=2(1/2)^{N}<r/(nw+1)$.

Let $x\in Q(F(N))$ and $y=x-s$, so $y_{k}=x_{k}-s_{k}$ for $k\in[n]$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations. Both $x_{k}$ and $s_{k}$ lie between $\alpha^{(N)}_{k}$ and $\beta^{(N)}_{k}$, so by (N2)

$$|y_{k}|\le\beta^{(N)}_{k}-\alpha^{(N)}_{k}=(b_{k}-a_{k})(1/2)^{N-1}\le w(1/2)^{N-1}\quad\text{for every }k\in[n].$$

By Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §coordinate, $\lVert y\rVert\le nw(1/2)^{N-1}\le(nw+1)(1/2)^{N-1}<r$. By Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §distance and symmetry of $d_{E}$, $d_{E}(s,x)=d_{E}(x,s)=\lVert x-s\rVert<r$, so $x\in B_{d_{E}}(s,r)$ by Open Ball in a Metric Space §membership, hence $x\in U$. As also $x\in Q$, $x\in Q\cap U=W$. Thus $Q(F(N))\subseteq W=\bigcup\{W\}$, and $\{W\}$ is a finite subset of $\mathcal{U}$ by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §small, so $Q(F(N))$ is small. This contradicts (N1).

Hence $Q$ is small: there is a finite subset $\mathcal{V}$ of $\mathcal{U}$ with $Q\subseteq\bigcup\mathcal{V}$. As $\mathcal{U}$ was arbitrary, $(Q,\mathcal{T}_{Q})$ is compact by Compact Topological Space and Compact Subset §compact, and $Q$ is compact in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$.