summaryrefslogtreecommitdiff
path: root/library/topology
diff options
context:
space:
mode:
Diffstat (limited to 'library/topology')
-rw-r--r--library/topology/real-topological-space.tex14
1 files changed, 11 insertions, 3 deletions
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index 8757ffb..1c5e4cb 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -132,9 +132,17 @@
\begin{proof}
$x - \epsilon \in \reals$.
$x + \epsilon \in \reals$.
-
- It suffices to show that for all $c$ such that $c \in \reals \land (x - \epsilon) < c < (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$.
- %Fix $c$ such that $c \in \reals \land (x - \epsilon) < c < (x + \epsilon)$.
+
+
+ %It suffices to show that for all $c$ such that $c \rless x$ we have $c \in \epsBall{x}{\epsilon}$.
+ %Fix $c$ such that $c \rless x$.
+%
+ %It suffices to show that for all $c$ such that $c < x$ we have $c \in \epsBall{x}{\epsilon}$.
+ %Fix $c$ such that $c < x$.
+
+
+ It suffices to show that for all $c$ such that $c \in \reals \land (x - \epsilon) \rless c \rless (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$.
+ Fix $c$ such that $(c \in \reals) \land (x - \epsilon) \rless c \rless (x + \epsilon)$.
%Suppose $(x - \epsilon) < c < (x + \epsilon)$.
\end{proof}