From 68716d1ab46dee3dfc1b03089f941dbb6883cdcd Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 4 Sep 2024 15:17:50 +0200
Subject: Mismatched Assume in Induction

Unexpeced Mismatch in line 99 and 109  or the pair
100 and 108. Parsing works with line 99 and 108 or with
the lines 100 and 109.

zf: MismatchedAssume (TermSymbol (SymbolPredicate (PredicateNoun (SgPl {sg = [Just (Word "natural"),Just (Word "number")], pl = [Just (Word "natural"),Just (Word "numbers")]}))) [TermVar (NamedVar "n")]) (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (NamedVar "n"),TermSymbol (SymbolMixfix [Just (Command "naturals")]) []]) (TermSymbol (SymbolPredicate (PredicateVerb (SgPl {sg = [Just (Word "has"),Just (Word "cardinality"),Nothing], pl = [Just (Word "ha"),Just (Word "cardinality"),Nothing]}))) [TermSymbol (SymbolMixfix [Just (Command "seq"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR,Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermSymbol (SymbolMixfix [Just (Command "emptyset")]) [],TermVar (NamedVar "n")],TermSymbol (SymbolMixfix [Just (Command "suc"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermVar (NamedVar "n")]]))
---
 library/topology/real-topological-space.tex | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 library/topology/real-topological-space.tex

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

diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
new file mode 100644
index 0000000..239965c
--- /dev/null
+++ b/library/topology/real-topological-space.tex
@@ -0,0 +1,26 @@
+\import{set.tex}
+\import{set/cons.tex}
+\import{set/powerset.tex}
+\import{set/fixpoint.tex}
+\import{set/product.tex}
+\import{topology/topological-space.tex}
+\import{topology/separation.tex}
+\import{topology/continuous.tex}
+\import{topology/basis.tex}
+\import{numbers.tex}
+\import{function.tex}
+
+
+\section{The canonical topology on $\mathbbR$}
+
+\begin{definition}\label{topological_basis_reals_eps_ball}
+    $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
+\end{definition}
+
+\begin{theorem}\label{reals_as_topo_space}
+    Suppose $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$.
+    Then $\reals$ is a topological space.
+\end{theorem}
+\begin{proof}
+    Omitted.
+\end{proof}
\ No newline at end of file
-- 
cgit v1.2.3