A subset of $\mathbb{R}^n$ with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology

Let $n \in \mathbb{N}$ with $n \ge 1$, let $\mathbb{R}^n$ be the set of functions $n \to \mathbb{R}$ ($\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$, and $d_1$, $d_2$, $d_\infty$ are metrics on it) carrying the product topology of $n$ copies of the usual topology of $\mathbb{R}$ (The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space), and let $d_2$ be the Euclidean metric. Then:

1. The product topology on $\mathbb{R}^n$ is the metric topology of $d_2$ (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement), so $\mathbb{R}^n$ as a product and $\mathbb{R}^n$ as a metric space are one topological space, and it is metrizable (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).
2. A subset $K \subseteq \mathbb{R}^n$ is a compact subset for the product topology (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) if and only if $K$ is closed in $\mathbb{R}^n$ and bounded (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

The hypothesis $n \ge 1$ is inherited from $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$, and $d_1$, $d_2$, $d_\infty$ are metrics on it, which defines $\mathbb{R}^n$ and its three metrics only there; for $n = 0$ the product is a one-point space and is compact. No choice principle is used: the metric statement it is read off from is proved by bisection (Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

This is a corollary in the strict sense. Nothing is reproved: claim 1 is For $n \ge 1$ the product topology on $n$ copies of the usual topology of $\mathbb{R}$ is the metric topology of $d_\infty$ on $\mathbb{R}^n$, and hence also of $d_1$ and $d_2$, so $\mathbb{R}^n$ as a product and $\mathbb{R}^n$ as a metric space are one space, the passage between the two readings of "compact subset" is For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide, and the mathematical content of claim 2 is Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line. What the corollary records is that the three fit together, so that a reader working in the product topology may use Heine-Borel without translating.

A second route to the compactness of a box. For reals $a_k \le b_k$ the box $\prod_{k<n} [a_k, b_k]$ is a product of finitely many compact spaces, each $[a_k,b_k]$ being compact by claim 2 applied with $n = 1$, so A product of finitely many compact spaces is compact in the product topology makes it compact using only the one-dimensional case of claim 2, and with it only the one-dimensional bisection. The two routes agree, as claim 1 requires; the bisection proof is the one that also delivers the converse.

Boundedness is metric and compactness is not. "Bounded" in claim 2 is a property of the metric $d_2$, not of the topology it induces: a metrizable space with at least two points carries, for every positive real $D$, a compatible metric of diameter $D$. What claim 2 says is that for this particular metric on this particular space the conjunction of closedness and boundedness detects compactness; the same conjunction fails to do so in a general metric space (FALSE: a closed and bounded subset of a metric space is compact).