From 99c65219a7edd1e71b6af868734f77b8dd002f7c Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Thu, 16 May 2024 15:40:25 +0200
Subject: Fix missing `\text`

---
 library/topology/basis.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/topology/basis.tex')

diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index bca42f0..ecdd0f7 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -45,6 +45,6 @@
 \end{definition}
 
 \begin{definition}\label{genOpens}
-    $\genOpens{B}{X} = \{ U\in\pow{X} \mid for all $x\in U$ there exists $V\in B$
-    such that $x\in V\subseteq U$\}$.
+    $\genOpens{B}{X} = \{ U\in\pow{X} \mid \text{for all $x\in U$ there exists $V\in B$
+    such that $x\in V\subseteq U$}\}$.
 \end{definition}
-- 
cgit v1.2.3


From d87aa179ade758a02a9b1609dadc07bf842df635 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 21 May 2024 19:23:59 +0200
Subject: Allow line breaks via `\textbox`, handle `\left`/`\right`

---
 latex/naproche.sty                 | 3 ++-
 library/topology/basis.tex         | 4 ++--
 source/Syntax/Concrete/Keywords.hs | 4 ++--
 source/Syntax/Token.hs             | 6 +++---
 4 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'library/topology/basis.tex')

diff --git a/latex/naproche.sty b/latex/naproche.sty
index 4bbefea..00ddf9a 100644
--- a/latex/naproche.sty
+++ b/latex/naproche.sty
@@ -11,7 +11,8 @@
 % command for importing theories, no visible rendering
 \newcommand{\import}[1]{}
 \newcommand{\explanation}[1]{\quad\text{[#1]}}
-
+\usepackage{pbox}
+\newcommand{\textbox}[1]{\pbox{28em}{#1}}
 
 
 
diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index ecdd0f7..e33909f 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -45,6 +45,6 @@
 \end{definition}
 
 \begin{definition}\label{genOpens}
-    $\genOpens{B}{X} = \{ U\in\pow{X} \mid \text{for all $x\in U$ there exists $V\in B$
-    such that $x\in V\subseteq U$}\}$.
+    $\genOpens{B}{X} = \left\{ U\in\pow{X} \middle| \textbox{for all $x\in U$ there exists $V\in B$
+    \\ such that $x\in V\subseteq U$}\right\}$.
 \end{definition}
diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Syntax/Concrete/Keywords.hs
index e0f577e..135cdac 100644
--- a/source/Syntax/Concrete/Keywords.hs
+++ b/source/Syntax/Concrete/Keywords.hs
@@ -203,7 +203,7 @@ _haveIntro = _thus <|> _particularly <|> _have
 _colon :: Prod r Text (Located Token) SourcePos
 _colon = symbol ":" ? ":"
 _pipe :: Prod r Text (Located Token) SourcePos
-_pipe = symbol "|" <|> command "mid" ? "\\mid"
+_pipe = (optional (command "middle") *> symbol "|") <|> command "mid" ? "\\mid"
 _comma :: Prod r Text (Located Token) SourcePos
 _comma = symbol "," ? ","
 _commaAnd :: Prod r Text (Located Token) SourcePos
@@ -219,4 +219,4 @@ _eq = symbol "=" ? "="
 _in :: Prod r Text (Located Token) SourcePos
 _in = symbol "∈" <|> command "in" ? "\\in"
 _subseteq :: Prod r Text (Located Token) SourcePos
-_subseteq = command "subseteq" ? ":"
+_subseteq = command "subseteq" ? "\\subseteq"
diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index eb0950f..65c02ca 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -228,7 +228,7 @@ mathToken =
 
 beginText :: Lexer (Located Token)
 beginText = lexeme do
-    Char.string "\\text{"
+    Char.string "\\text{" <|> Char.string "\\textbox{"
     setTextMode
     pure (BeginEnv "text")
 
@@ -249,14 +249,14 @@ textToken = word <|> symbol <|> begin <|> end <|> textEnd <|> mathBegin <|> alig
             setMathMode
             pure (EndEnv "text")
 
-        opening' = lexeme (brace <|> group <|> paren <|> bracket)
+        opening' = lexeme (group <|> optional (Char.string "\\left") *> (brace <|> paren <|> bracket))
             where
                 brace = VisibleBraceL <$ lexeme (Char.string "\\{")
                 group = InvisibleBraceL <$ lexeme (Char.char '{') <* modify' incrNesting
                 paren = ParenL <$ lexeme (Char.char '(')
                 bracket = BracketL <$ lexeme (Char.char '[')
 
-        closing' = lexeme (brace <|> group <|> paren <|> bracket)
+        closing' = lexeme (group <|> optional (Char.string "\\right") *> (brace <|> paren <|> bracket))
             where
                 brace = VisibleBraceR <$ lexeme (Char.string "\\}")
                 group = InvisibleBraceR <$ lexeme (Char.char '}') <* modify' decrNesting
-- 
cgit v1.2.3


From 311fff704f96869e0ea239f129a7cf846c206c4f Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 22 May 2024 16:57:17 +0200
Subject: Update label for `genopens`

---
 library/topology/basis.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/topology/basis.tex')

diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index e33909f..d8cfeaf 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -44,7 +44,7 @@
     there exists $W\in B$ such that $x\in W\subseteq U, V$.
 \end{definition}
 
-\begin{definition}\label{genOpens}
+\begin{definition}\label{genopens}
     $\genOpens{B}{X} = \left\{ U\in\pow{X} \middle| \textbox{for all $x\in U$ there exists $V\in B$
     \\ such that $x\in V\subseteq U$}\right\}$.
 \end{definition}
-- 
cgit v1.2.3


From 3ae13f68d8d572aa62982bde614acf79dff60848 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 28 May 2024 17:27:29 +0200
Subject: Update `inters_in_genopens`

---
 library/topology/basis.tex | 35 +++++++++++------------------------
 1 file changed, 11 insertions(+), 24 deletions(-)

(limited to 'library/topology/basis.tex')

diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index 15910f9..4f66166 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -75,45 +75,32 @@
 \end{proof}
 
 
-
-
 \begin{lemma}\label{inters_in_genopens}
     Assume $B$ is a topological basis for $X$.
-    %For all $A, C$ 
-    If $A\in \genOpens{B}{X}$ and $C\in \genOpens{B}{X}$ then $(A\inter C) \in \genOpens{B}{X}$.
+    Assume $A, C\in \genOpens{B}{X}$.
+    Then $(A\inter C) \in \genOpens{B}{X}$.
 \end{lemma}
 \begin{proof}
-    
-    Show $(A \inter C) \in \pow{X}$.
-    \begin{subproof}
-        $(A \inter C) \subseteq X$ by assumption.
-    \end{subproof}
-    Therefore for all $A, C \in \genOpens{B}{X}$ we have $(A \inter C) \in \pow{X}$.
-    
+
+    We have $(A \inter C) \in \pow{X}$ by \cref{genopens,inter_powerset}.
 
     Show for all $x\in (A\inter C)$ there exists $W \in B$
     such that $x\in W$ and $W \subseteq (A\inter C)$.
     \begin{subproof}
         Fix $x \in (A\inter C)$.
-        There exist $V' \in B$ such that $x \in V'$ and $V' \subseteq A$ by assumption.  %TODO: Warum muss hier by assumtion hin?
-        There exist $V'' \in B$ such that $x \in V''$ and $V'' \subseteq C$ by assumption.
-        There exist $W \in B$ such that $x \in W$ and $W \subseteq v'$ and $W \subseteq V''$ by assumption.
-        
+        Then $x\in A,C$.
+        There exists $V'  \in B$ such that $x \in V' \subseteq A$ by \cref{genopens}.
+        There exists $V'' \in B$ such that $x \in V''\subseteq C$ by \cref{genopens}.
+        There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$.
+
         Show $W \subseteq (A\inter C)$.
         \begin{subproof}
             %$W \subseteq v'$ and $W \subseteq V''$.
-            For all $y \in W$ we have $y \in V'$ and $y \in V''$ by assumption.
+            For all $y \in W$ we have $y \in V'$ and $y \in V''$.
         \end{subproof}
     \end{subproof}
     %Therefore for all $A, C, x$ such that $A \in \genOpens{B}{X}$ and $C \in \genOpens{B}{X}$ and $x \in (A \inter C)$ we have there exists $W \in B$
     %such that $x\in W$ and $W \subseteq (A\inter C)$.
 
-    $(A\inter C) \in \genOpens{B}{X}$ by assumption.
-    
- 
+    $(A\inter C) \in \genOpens{B}{X}$.
 \end{proof}
-
-
-
-
-
-- 
cgit v1.2.3

