Hopf–Rinow theorem

Condition 1 implies condition 2 by [F3].

Suppose condition 2 holds. For $p\in M$ and $v\in T_{p}M$, [F2] gives $I_{p,v}=\mathbb{R}$, so in particular $1\in I_{p,v}$ and hence $v\in {\mathcal{E}}_p$. Thus $T_{p}M\subseteq {\mathcal{E}}_p$; the reverse inclusion is part of the definition, so ${\mathcal{E}}_p=T_{p}M$. Since $p$ was arbitrary, condition 3 holds.

Suppose condition 3 holds. Nonemptiness supplies one point $p_0\in M$, and condition 3 at that one point gives ${\mathcal{E}}_{p_0}=T_{p_0}M$. Thus condition 4 holds. This instantiates one existential statement and makes no family of choices.

Suppose condition 4, and fix such a $p_0$. Let $S\subseteq M$ be closed and bounded. If $S=\mathrm{\varnothing }$, every open cover has the empty finite subcover, so $S$ is compact. Suppose instead that $S\mathrm{\ne }\mathrm{\varnothing }$. By [F4] there are $a\in M$ and $r>0$ such that $S\subseteq B(a,r)$, and put $R=d(p_0,a)+r>0,K_R=\{v\in T_{p_0}M:\mathrm{\mid }v{\mathrm{\mid }}_{g_{p_0}}\le R\}\mathrm{.}$ For $q\in S$, the triangle inequality gives $d(p_0,q)\le d(p_0,a)+d(a,q)<R$.

If $\dim M>0$, identify $T_{p_0}M$ with ${\mathbb{R}}^n$ by one orthonormal basis from [F5]. The identity $\mathrm{\mid }{\sum }_i{u}^i{e}_i{\mathrm{\mid }}^2={\sum }_i(u^i{)}^2$ identifies $K_R$ with the Euclidean closed ball of radius $R$, which is closed and bounded and therefore compact by [F5]. If $\dim M=0$, then $T_{p_0}M=\{0_{p_0}\}$ and $K_R$ is a singleton; given an open cover, any member containing its sole point is a one-member finite subcover. Thus $K_R$ is compact in every dimension.

Suppose condition 5, and let $(x_k)$ be a Cauchy sequence in $(M,d)$. By [F7] there are $c\in M$ and $r>0$ such that every $x_k$ lies in $B(c,r)$. Put $C=\bar{B}(c,r)$. It is closed by [F4], and it is bounded because $C\subseteq B(c,r+1)$. Hence condition 5 makes $C$ compact.

The theorem assumes ${\mathrm{A}\mathrm{C}}_{\omega }$ because the maximal-geodesic and radial-minimizer facts [F2] and [F3] use the global geodesic construction under that assumption.

The smooth exponential-map fact [F6] inherits the same ${\mathrm{A}\mathrm{C}}_{\omega }$ assumption and introduces no stronger choice principle.

For this fixed $q$, [F3] supplies a vector $v_q\in T_{p_0}M$ with ${\exp }_{p_0}(v_q)=q$ and $\mathrm{\mid }{v}_q{\mathrm{\mid }}_{g_{p_0}}=d(p_0,q)<R$. Hence $q\in {\exp }_{p_0}[K_R]$. Since $q$ was arbitrary, $S\subseteq {\exp }_{p_0}[K_R]\mathrm{.}$ This pointwise use of an existential theorem proves an inclusion; it does not construct or use a choice function $q\mapsto v_q$.

By [F7], the metric subspace $(C,d{\mathrm{\mid }}_{C\times C})$ is a compact metric space and therefore complete. The sequence $(x_k)$ is Cauchy in this subspace, because all its terms lie in $C$ and the subspace distance is the same $d$. It consequently converges to some $x\in C$ in the subspace metric, hence also in $(M,d)$. Every Cauchy sequence in $M$ converges in $M$, so condition 1 holds.

The map ${\exp }_{p_0}$ is continuous on all of $T_{p_0}M$ by condition 4 and [F6], so $H_R:={\exp }_{p_0}[K_R]$ is compact. Since $S$ is closed in $M$, it is closed in the subspace $H_R$; steps 2.1 and 1.5 and [F6] therefore make $S$ compact. The closed bounded set $S$ was arbitrary, so condition 5 holds.

Steps 1.1--3.1 and 1.6--2.2 prove the cycle $1⟹2⟹3⟹4⟹5⟹1,$ so all five conditions are equivalent.

Assume any one of the equivalent conditions and fix $x,y\in M$. Condition 3 then holds, so ${\mathcal{E}}_x=T_{x}M$. Because $M$ is connected, the component of $x$ is all of $M$, and [F3] supplies $v\in T_{x}M$ with the stated endpoint, norm, length, and global minimizing properties. This proves the final assertion.

Step 1.4 treats the empty closed bounded subset separately and keeps every ball radius positive; step 1.5 uses the closed tangent-ball endpoint. Both directions of the equivalence are present in the cycle.

Nonemptiness was used exactly at step 1.3 and is indispensable for the displayed equivalence, as the statement's empty-manifold comparison shows. A nonempty connected zero-manifold is a singleton: its zero-dimensional charts make points open, and a discrete connected nonempty space has one point. All five conditions then hold and step 5.1 gives the constant minimizing geodesic. The proof in dimension one is unchanged. At $x=y$, [F3] supplies $v=0_x$, so no division by a distance occurs.

The finite-dimensional and topological compactness facts in [F5]--[F7] require no additional choice. The constructions in steps 1.4--3.1 use only fixed existential witnesses or pointwise existential elimination, as step 2.1 makes explicit, and therefore add no countable or arbitrary selection.