From 3ef20da08eda23db76d763a2c6c7ee416348a021 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 15 Sep 2024 19:05:25 +0200
Subject: Fix Assume Issue

At line 137 in real-topological-space.tex
Can't use Fix at this point.
---
 library/numbers.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index b7de307..73eefc8 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -718,7 +718,7 @@ Laws of the order on the reals
 \end{proof}
 
 \begin{lemma}\label{reals_minus}
-    Assume $x,y \in \reals$. If $x \rminus y = \zero$ then $x=y$.
+    Assume $x,y \in \reals$. If $x - y = \zero$ then $x=y$.
 \end{lemma}
 \begin{proof}
     Omitted.
@@ -803,7 +803,7 @@ Laws of the order on the reals
 \end{definition}
 
 \begin{definition}\label{realsplus}
-    $\realsplus = \reals \setminus \realsminus$.
+    $\realsplus = \{r \in \reals \mid r > \zero\}$.
 \end{definition}
 
 \begin{definition}\label{epsilon_ball}
-- 
cgit v1.2.3