From 640fe16eaab00ea29046ef18e6f751571d923eaa Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 16 Sep 2024 02:12:06 +0200
Subject: Missmatched Assume Error found. not fixed

In line 137 and 140 of real-topological-space.tex
Line 140 wont get parsed and line 140 will get parsed.

Case matching in Checking.hs is not working as intended.
Case phi@(Atomic p args) ->    in line 960 in checking.hs
is not reached in checking of the Fixing with a symbol

Error Massage shows that < will be interpreted as a Term symbol there
not as a predicate.

Error Massage:
zf: MismatchedAssume (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "<"))) [TermVar (NamedVar "c"),TermVar (NamedVar "x")]) (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "rless"))) [TermVar (NamedVar "c"),TermVar (NamedVar "x")]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (NamedVar "c"),TermSymbol (SymbolMixfix [Just (Command "epsBall"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR,Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermVar (NamedVar "x"),TermVar (NamedVar "epsilon")]]))
---
 library/topology/real-topological-space.tex | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'library/topology/real-topological-space.tex')

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}
 
-- 
cgit v1.2.3