Proof of The Heine-Borel Theorem in $\mathbb{R}^n$, and Compactness of Closed Balls and the Unit Sphere

Each result cited is universally quantified over the data in its own statement.

Let $n$, $\lVert\cdot\rVert$ and $d_{E}$ be as in the statement. By $\mathbb{R}^n$ with the Euclidean Distance Is a Complete Metric Space with Coordinatewise Convergence §metric, $(\mathbb{R}^{n},d_{E})$ is a metric space, so $d_{E}$ satisfies Metric Space §nonnegative, Metric Space §symmetric and Metric Space §triangle; $\mathcal{T}_{d_{E}}$ is the topology of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §topology, so $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$ is a topological space, and a subset of $\mathbb{R}^{n}$ lies in $\mathcal{T}_{d_{E}}$ exactly when it is open in $(\mathbb{R}^{n},d_{E})$. Components are as in Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership.

Clause heine-borel. Let $A\subseteq\mathbb{R}^{n}$.

If $A$ is compact in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$, then it is closed in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$ and bounded in $(\mathbb{R}^{n},d_{E})$ by Closed Subsets of Compact Sets Are Compact, and Compact Subsets of a Metric Space Are Closed and Bounded §closed-bounded, applied to the metric space $(\mathbb{R}^{n},d_{E})$.

Conversely, let $A$ be closed in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$ and bounded in $(\mathbb{R}^{n},d_{E})$. We first find $c\in\mathbb{R}^{n}$ and a real $R\ge0$ with $d_{E}(c,x)\le R$ for every $x\in A$. If $A=\emptyset$, take $c=0$, the origin of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §origin, and $R=0$. Otherwise let $c\in A$ and, by Bounded Subset of a Metric Space §bounded, let $R$ be a real number with $d_{E}(u,v)\le R$ for all $u,v\in A$; then $d_{E}(c,x)\le R$ for $x\in A$, and $R\ge d_{E}(c,c)\ge0$.

Let $a,b\in\mathbb{R}^{n}$ be the maps $k\mapsto c_{k}-R$ and $k\mapsto c_{k}+R$ 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, as $c_{k}-R\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §negative, 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, 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 §operation-substitution 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 §difference-formula. Then $a_{k}\le b_{k}$ for every $k\in[n]$, and with

$$Q=\{x\in\mathbb{R}^{n}:a_{k}\le x_{k}\le b_{k}\text{ for every }k\in[n]\},$$

$Q$ is compact in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$ by Closed Boxes in $\mathbb{R}^n$ Are Compact §box. Moreover $A\subseteq Q$: for $x\in A$ and $k\in[n]$, $(x-c)_{k}=x_{k}-c_{k}$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations, so by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §coordinate and Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §distance,

$$|x_{k}-c_{k}|\le\lVert x-c\rVert=d_{E}(x,c)=d_{E}(c,x)\le R,$$

that is $a_{k}\le x_{k}\le b_{k}$. Since $A\subseteq Q$ and $A$ is closed in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$, Closed Subsets of Compact Sets Are Compact, and Compact Subsets of a Metric Space Are Closed and Bounded §closed-subset, applied to the topological space $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$, the compact set $Q$ and the closed subset $A$, shows that $A$ is compact in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$.

Clause balls. Let $c\in\mathbb{R}^{n}$ and $r\in\mathbb{R}$ with $r\ge0$, and let $\bar{B}=\bar{B}_{d_{E}}(c,r)$, so that for $y\in\mathbb{R}^{n}$, $y\in\bar{B}$ if and only if $d_{E}(c,y)\le r$, by Closed Ball in a Metric Space §membership.

$\bar{B}$ is closed. Let $y\in\mathbb{R}^{n}\setminus\bar{B}$, so $r<d_{E}(c,y)$, and let $\varepsilon=d_{E}(c,y)-r>0$, a real number by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §negative. For $z$ in the open ball $B_{d_{E}}(y,\varepsilon)$, $d_{E}(y,z)<\varepsilon$ by Open Ball in a Metric Space §membership, and $d_{E}(c,y)\le d_{E}(c,z)+d_{E}(z,y)=d_{E}(c,z)+d_{E}(y,z)$, so

$$d_{E}(c,z)\ge d_{E}(c,y)-d_{E}(y,z)>d_{E}(c,y)-\varepsilon=r,$$

and $z\notin\bar{B}$. Thus $B_{d_{E}}(y,\varepsilon)\subseteq\mathbb{R}^{n}\setminus\bar{B}$, so $\mathbb{R}^{n}\setminus\bar{B}$ is open in $(\mathbb{R}^{n},d_{E})$ by Open Subset of a Metric Space §open, hence lies in $\mathcal{T}_{d_{E}}$, and $\bar{B}$ is closed in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$.

$\bar{B}$ is bounded. For $u,v\in\bar{B}$, $d_{E}(u,v)\le d_{E}(u,c)+d_{E}(c,v)=d_{E}(c,u)+d_{E}(c,v)\le2r$ (with $2=1+1$ in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §two), so $\bar{B}$ is bounded in $(\mathbb{R}^{n},d_{E})$.

By the clause heine-borel, proved above, $\bar{B}$ is compact in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$.

Clause sphere. Let $S=\{x\in\mathbb{R}^{n}:\lVert x\rVert=1\}$.

$S$ is closed. Let $y\in\mathbb{R}^{n}\setminus S$, so $\lVert y\rVert\neq1$, and let $\varepsilon=|\lVert y\rVert-1|>0$, a real number by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §negative and Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §absolute-value. Let $z\in B_{d_{E}}(y,\varepsilon)$, so $d_{E}(y,z)<\varepsilon$ by Open Ball in a Metric Space §membership. By Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §reverse-triangle and Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §distance,

$$\bigl|\lVert z\rVert-\lVert y\rVert\bigr|\le\lVert z-y\rVert=d_{E}(z,y)=d_{E}(y,z)<\varepsilon.$$

If $\lVert z\rVert=1$, this would read $|1-\lVert y\rVert|<\varepsilon=|\lVert y\rVert-1|=|1-\lVert y\rVert|$, which is impossible; so $z\notin S$. Thus $B_{d_{E}}(y,\varepsilon)\subseteq\mathbb{R}^{n}\setminus S$, so $\mathbb{R}^{n}\setminus S$ is open in $(\mathbb{R}^{n},d_{E})$ by Open Subset of a Metric Space §open, hence lies in $\mathcal{T}_{d_{E}}$, and $S$ is closed in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$ by Closed Subset of a Topological Space §closed.

$S$ is bounded. For $u,v\in S$, with $0$ the origin of Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §origin, $d_{E}(u,0)=\lVert u\rVert=1$ and $d_{E}(v,0)=\lVert v\rVert=1$ by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §distance, so $d_{E}(u,v)\le d_{E}(u,0)+d_{E}(0,v)=d_{E}(u,0)+d_{E}(v,0)=2$, with $2=1+1$ in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §two.

By the clause heine-borel, $S$ is compact in $(\mathbb{R}^{n},\mathcal{T}_{d_{E}})$.

No choice principle is used: the only existential instantiations are $c$ and $R$.