diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-09-16 02:12:06 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-09-16 02:12:06 +0200 |
| commit | 640fe16eaab00ea29046ef18e6f751571d923eaa (patch) | |
| tree | a15b2538f9895f54669251cd0ddf05c35ccf77d7 | |
| parent | 3ef20da08eda23db76d763a2c6c7ee416348a021 (diff) | |
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")]]))
| -rw-r--r-- | library/topology/real-topological-space.tex | 14 |
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} |