Merge pull request #1168 from lowasser/patch-1

Simplify Cauchy completeness of Dedekind reals

Author: mikeshulman

reals.tex

@@ -518,35 +518,23 @@ \subsection{Dedekind reals are Cauchy complete}
     U_y(q) &\defeq \exis{\epsilon, \theta : \Qp} U_{x_\epsilon}(q - \epsilon - \theta).
   \end{align*}
   %
-  It is clear that $L_y$ and $U_y$ are inhabited, rounded, and disjoint. To establish
-  locatedness, consider any $q, r : \Q$ such that $q < r$. There is $\epsilon : \Qp$ such
-  that $5 \epsilon < r - q$. Since $q + 2 \epsilon < r - 2 \epsilon$ merely
+  It is clear that $L_y$ and $U_y$ are inhabited and rounded.  Disjointness follows from
+  the Cauchy approximation condition. To establish locatedness, consider any 
+  $q, r : \Q$ such that $q < r$. There is $\epsilon : \Qp$ such that 
+  $4 \epsilon < r - q$. Since $q + 2 \epsilon < r - 2 \epsilon$ merely
   $L_{x_\epsilon}(q + 2 \epsilon)$ or $U_{x_\epsilon}(r - 2 \epsilon)$. In the first case
   we have $L_y(q)$ and in the second $U_y(r)$.
 
   To show that $y$ is the limit of $x$, consider any $\epsilon, \theta : \Qp$. Because
   $\Q$ is dense in $\RD$ there merely exist $q, r : \Q$ such that
   %
   \begin{narrowmultline*}
-    x_\epsilon - \epsilon - \theta/2 < q < x_\epsilon - \epsilon - \theta/4
+    x_\epsilon - \epsilon - \theta < q < x_\epsilon - \epsilon - \theta/2
     < x_\epsilon < \\
-    x_\epsilon + \epsilon + \theta/4 < r < x_\epsilon + \epsilon + \theta/2,
+    x_\epsilon + \epsilon + \theta/2 < r < x_\epsilon + \epsilon + \theta,
   \end{narrowmultline*}
   %
-  and thus $q < y < r$. Now either $y < x_\epsilon + \theta/2$ or $x_\epsilon - \theta/2 < y$.
-  In the first case we have
-  %
-  \begin{equation*}
-    x_\epsilon - \epsilon - \theta/2 < q < y < x_\epsilon + \theta/2,
-  \end{equation*}
-  %
-  and in the second
-  %
-  \begin{equation*}
-    x_\epsilon - \theta/2 < y < r < x_\epsilon + \epsilon + \theta/2.
-  \end{equation*}
-  %
-  In either case it follows that $|y - x_\epsilon| < \epsilon + \theta$.
+  and thus $q < y < r$. It follows that $|y - x_\epsilon| < \epsilon + \theta$.
 \end{proof}
 
 For sake of completeness we record the classic formulation as well.