Injectivity radius at a point and of a manifold

The set ${\mathcal{R}}_p$ is nonempty: by [F1], an open exponential-diffeomorphism domain contains some ball $B_r(0_p)$ with $r>0$, and restricting a diffeomorphism to that ball remains a diffeomorphism onto its open image. It is downward closed among positive radii. Hence its supremum is a well-defined element of $(0,+\mathrm{\infty }]$; it is $+\mathrm{\infty }$ exactly when admissible radii are unbounded.

If $M$ is nonempty, the set of positive pointwise radii has an infimum in $[0,+\mathrm{\infty }]$; it may be zero even though every term is positive. For $M=\mathrm{\varnothing }$, the stated empty-infimum convention gives $\mathrm{inj}(M)=+\mathrm{\infty }$. In dimension zero, $T_{p}M=\{0_p\}$ and every positive-radius ball is that singleton, so ${\mathcal{R}}_p=(0,\mathrm{\infty })$ and $\mathrm{inj}(p)=+\mathrm{\infty }$; dimension one uses the displayed formula unchanged. The balls are open, so their sphere endpoints are not included, while $0_p$ is always included. ${\mathrm{A}\mathrm{C}}_{\omega }$ is used only through [F1], not in taking the uniquely determined supremum or infimum.