From acbd09c738a26937dc9be4452843ea29ad190a11 Mon Sep 17 00:00:00 2001 From: Quirin Schroll Date: Tue, 1 Jul 2025 17:08:18 +0200 Subject: [PATCH 1/2] =?UTF-8?q?Zero-based=20indexing=20in=20=CE=B5-net=20d?= =?UTF-8?q?efinition?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- reals.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/reals.tex b/reals.tex index 72b7a8fb..e6e54748 100644 --- a/reals.tex +++ b/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} From ecb17fbc40889edc464d43735b3f7bc1a8504236 Mon Sep 17 00:00:00 2001 From: Quirin Schroll Date: Tue, 1 Jul 2025 17:08:59 +0200 Subject: [PATCH 2/2] Errata for acbd09c738a26937dc9be4452843ea29ad190a11 --- errata.tex | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/errata.tex b/errata.tex index 9f6724f7..3c86036b 100644 --- a/errata.tex +++ b/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)}$.\\