Make definition of ε-net use zero-based indexing

errata.tex

@@ -931,6 +931,10 @@
   & 1270-g3f17b85
   & In the proof, $n : \N$ should be $k : \N$. And the range of $i$ should be $0 \leq i \leq k$. Also in the last equation, $r(\lim x) = \ell$ should be $\lim x = \ell$.\\
   %
+  \cref{defn:total-bounded-metric-space}
+  & % merge of acbd09c738a26937dc9be4452843ea29ad190a11
+  & In the definition of an $\epsilon$-net, the finite sequences $x_1, \dots, x_n$ should use zero-based indexing: $x_0, \dots, x_n$\\
+  %
   \cref{sec:surreals}
   & 1189-ga9c35f0
   & The inductive case of $\iota_{\Q_D}$ should be defined as $\iota_{\Q_D}(a/2^n) \defeq \surr{\iota_{\Q_D}(a/2^n - 1/2^n)}{\iota_{\Q_D}(a/2^n + 1/2^n)}$.\\

reals.tex

@@ -1963,11 +1963,11 @@ \section{Compactness of the interval}
   d)$ is an element of
   %
   \begin{equation*}
-    \sm{n : \N}{x_1, \ldots, x_n : M}
+    \sm{n : \N}{x_0, \ldots, x_n : M}
     \fall{y : M} \exis{k \leq n} d(x_k, y) < \epsilon.
   \end{equation*}
   %
-  In words, this is a finite sequence of points $x_1, \ldots, x_n$ such that every point
+  In words, this is a finite sequence of points $x_0, \ldots, x_n$ such that every point
   in $M$ merely is within $\epsilon$ of some~$x_k$.
 
   A metric space $(M, d)$ is \define{totally bounded}
@@ -1978,13 +1978,13 @@ \section{Compactness of the interval}
   %
   \begin{equation*}
     \prd{\epsilon : \Qp}
-    \sm{n : \N}{x_1, \ldots, x_n : M}
+    \sm{n : \N}{x_0, \ldots, x_n : M}
     \fall{y : M} \exis{k \leq n} d(x_k, y) < \epsilon.
   \end{equation*}
 \end{defn}
 
 \begin{rmk}
-  In the definition of total boundedness we used sloppy notation $\sm{n : \N}{x_1, \ldots, x_n : M}$. Formally, we should have written $\sm{x : \lst{M}}$ instead,
+  In the definition of total boundedness we used sloppy notation $\sm{n : \N}{x_0, \ldots, x_n : M}$. Formally, we should have written $\sm{x : \lst{M}}$ instead,
   where $\lst{M}$ is the inductive type of finite lists\index{type!of lists} from \cref{sec:bool-nat}.
   However, that would make the rest of the statement a bit more cumbersome to express.
 \end{rmk}