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(-)

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 59cec853a697a4dd793c216c9bd603bd775d6da2 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Thu, 16 May 2024 15:59:04 +0200
Subject: Attach whitespace info to located token

---
 source/Syntax/Adapt.hs | 12 ++++++++----
 source/Syntax/Token.hs | 50 ++++++++++++++++++++++++++++++++------------------
 2 files changed, 40 insertions(+), 22 deletions(-)

diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index b1237d2..3a8b3d6 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -26,10 +26,14 @@ scanChunk ltoks =
     let toks = unLocated <$> ltoks
         matchOrErr re env pos = match re toks ?? error ("could not find lexical pattern in " <> env <> " at " <> sourcePosPretty pos)
     in case ltoks of
-        Located pos (BeginEnv "definition") : _ -> matchOrErr definition "definition" pos
-        Located pos (BeginEnv "abbreviation") : _ -> matchOrErr abbreviation "abbreviation" pos
-        Located pos (BeginEnv "struct") :_ -> matchOrErr struct "struct definition" pos
-        Located pos (BeginEnv "inductive") :_ -> matchOrErr inductive "inductive definition" pos
+        Located{startPos = pos, unLocated = BeginEnv "definition"} : _ ->
+            matchOrErr definition "definition" (pos)
+        Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ ->
+            matchOrErr abbreviation "abbreviation" pos
+        Located{startPos = pos, unLocated = (BeginEnv "struct")} :_ ->
+            matchOrErr struct "struct definition" pos
+        Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ ->
+            matchOrErr inductive "inductive definition" pos
         _ -> []
 
 adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon
diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index 1d13693..eb0950f 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -164,8 +164,17 @@ instance Pretty Token where
 data Located a = Located
     { startPos :: !SourcePos
     , unLocated :: !a
+    , postWhitespace :: Whitespace
     } deriving (Show)
 
+data Whitespace = NoSpace | Space deriving (Show)
+
+collapseWhitespace :: [Whitespace] -> Whitespace
+collapseWhitespace = \case
+    Space : _ -> Space
+    NoSpace : ws -> collapseWhitespace ws
+    [] -> NoSpace
+
 instance Eq a  => Eq  (Located a) where (==) = (==) `on` unLocated
 instance Ord a => Ord (Located a) where compare = compare `on` unLocated
 
@@ -178,32 +187,32 @@ toks = whitespace *> goNormal id <* eof
             r <- optional tok
             case r of
                 Nothing -> pure (f [])
-                Just t@(Located _ (BeginEnv "math")) -> goMath (f . (t:))
-                Just t@(Located _ (BeginEnv "align*")) -> goMath (f . (t:))
+                Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:))
+                Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:))
                 Just t -> goNormal (f . (t:))
         goText f = do
             r <- optional textToken
             case r of
                 Nothing -> pure (f [])
-                Just t@(Located _ (BeginEnv "math")) -> goMathInText (f . (t:))
-                Just t@(Located _ (EndEnv "text")) -> goMath (f . (t:))
-                Just t@(Located _ (EndEnv "explanation")) -> goMath (f . (t:))
+                Just t@Located{unLocated = BeginEnv "math"} -> goMathInText (f . (t:))
+                Just t@Located{unLocated = EndEnv "text"} -> goMath (f . (t:))
+                Just t@Located{unLocated = EndEnv "explanation"} -> goMath (f . (t:))
                 Just t -> goText (f . (t:))
         goMath f = do
             r <- optional mathToken
             case r of
                 Nothing -> pure (f [])
-                Just t@(Located _ (EndEnv "math")) -> goNormal (f . (t:))
-                Just t@(Located _ (EndEnv "align*")) -> goNormal (f . (t:))
-                Just t@(Located _ (BeginEnv "text")) -> goText (f . (t:))
-                Just t@(Located _ (BeginEnv "explanation")) -> goText (f . (t:))
+                Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:))
+                Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:))
+                Just t@Located{unLocated = BeginEnv "text"} -> goText (f . (t:))
+                Just t@Located{unLocated = BeginEnv "explanation"} -> goText (f . (t:))
                 Just t -> goMath (f . (t:))
         goMathInText f = do
             r <- optional mathToken
             case r of
                 Nothing -> pure (f [])
-                Just t@(Located _ (EndEnv "math")) -> goText (f . (t:))
-                Just t@(Located _ (BeginEnv "text")) -> goText (f . (t:))
+                Just t@(Located{unLocated = EndEnv "math"}) -> goText (f . (t:))
+                Just t@(Located{unLocated = BeginEnv "text"}) -> goText (f . (t:))
                 Just t -> goMathInText (f . (t:))
 {-# INLINE toks #-}
 
@@ -430,12 +439,17 @@ lexeme :: Lexer a -> Lexer (Located a)
 lexeme p = do
     start <- getSourcePos
     t <- p
-    whitespace
-    pure (Located start t)
+    w <- whitespace
+    pure (Located start t w)
 
-space :: Lexer ()
-space = void (Char.char ' ' <|> Char.char '\n' <|> Char.char '\r')
-    <|> void (Char.string "\\ " <|> Char.string "\\\\" <|> Char.string "\\!" <|> Char.string "\\," <|> Char.string "\\:" <|> Char.string "\\;" <|> Char.string "\\;")
+space :: Lexer Whitespace
+space = Space <$ (Char.char ' ' <|> Char.char '\n' <|> Char.char '\r')
+    <|> Space <$ (Char.string "\\ " <|> Char.string "\\\\" <|> Char.string "\\!" <|> Char.string "\\," <|> Char.string "\\:" <|> Char.string "\\;" <|> Char.string "\\;")
 
-whitespace :: Lexer ()
-whitespace = Lexer.space (void (some space)) (Lexer.skipLineComment "%") empty
+whitespace :: Lexer Whitespace
+whitespace = do
+    ws <- many (spaces <|> comment)
+    pure (collapseWhitespace ws)
+    where
+        spaces = collapseWhitespace <$> some space
+        comment = NoSpace <$ Lexer.skipLineComment "%"
-- 
cgit v1.2.3


From 3845ab9020b3eb591ef999827503b483eb735bd7 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 21 May 2024 16:52:01 +0200
Subject: Add simple lemmas on filters

---
 library/set.tex        | 10 ++++++----
 library/set/filter.tex | 29 +++++++++++++++++++++++------
 2 files changed, 29 insertions(+), 10 deletions(-)

diff --git a/library/set.tex b/library/set.tex
index 33e5af4..e7e062f 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -553,13 +553,15 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Follows by set extensionality.
 \end{proof}
 
-\begin{proposition}%
-\label{inter_subseteq}
+\begin{proposition}\label{inter_subseteq_left}
     $A\inter B\subseteq A$.
 \end{proposition}
 
-\begin{proposition}%
-\label{inter_emptyset}
+\begin{proposition}\label{inter_subseteq_right}
+    $A\inter B\subseteq B$.
+\end{proposition}
+
+\begin{proposition}\label{inter_emptyset}
     $A\inter\emptyset = \emptyset$.
 \end{proposition}
 \begin{proof}
diff --git a/library/set/filter.tex b/library/set/filter.tex
index 2797d86..93309de 100644
--- a/library/set/filter.tex
+++ b/library/set/filter.tex
@@ -3,6 +3,8 @@
 
 \section{Filters}
 
+\subsection{Definition and basic properties of filters}
+
 \begin{abbreviation}\label{upwardclosed}
     $F$ is upward-closed in $S$ iff
     for all $A, B$ such that $A\subseteq B\subseteq S$ and $A\in F$ we have $B\in F$.
@@ -11,22 +13,37 @@
 \begin{definition}\label{filter}
     $F$ is a filter on $S$ iff
     $F$ is a family of subsets of $S$
-    and $S$ is inhabited
     and $S\in F$
     and $\emptyset\notin F$
     and $F$ is closed under binary intersections
     and $F$ is upward-closed in $S$.
 \end{definition}
 
+\begin{proposition}\label{filter_ext_complement}
+    Let $F, G$ be filters on $S$.
+    Suppose for all $A\subseteq S$ we have $S\setminus A\in F$ iff $S\setminus A\in G$.
+    Then $F = G$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{filter_inter_in_iff}
+    Let $F$ be a filter on $S$.
+    Suppose $A, B\subseteq S$.
+    Then $A\inter B\in F$ iff $A, B\in F$.
+\end{proposition}
+\begin{proof}
+    We have $A\inter B\subseteq A, B$.
+    Follows by \cref{filter}.
+\end{proof}
+
+\subsection{Principal filters over a set}
+
 \begin{definition}\label{principalfilter}
     $\principalfilter{S}{A} = \{X\in\pow{S}\mid A\subseteq X\}$.
 \end{definition}
 
-%\begin{proposition}\label{principalfilter_domain_inhabited}
-%    Suppose $F$ is a filter on $S$.
-%    Then $S$ is inhabited.
-%\end{proposition}
-
 \begin{proposition}\label{principalfilter_is_filter}
     Suppose $A\subseteq S$.
     Suppose $A$ is inhabited.
-- 
cgit v1.2.3


From 1ea35d4861f29faa5d7eab25c7773c0d9b638b38 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 21 May 2024 16:52:15 +0200
Subject: Add definition for `\genOpens`

---
 latex/naproche.sty | 1 +
 1 file changed, 1 insertion(+)

diff --git a/latex/naproche.sty b/latex/naproche.sty
index 9764693..4bbefea 100644
--- a/latex/naproche.sty
+++ b/latex/naproche.sty
@@ -87,6 +87,7 @@
 \newcommand{\fld}[1]{\fun{field}#1}
 \newcommand{\fst}[1]{\fun{fst}#1}
 \newcommand{\funs}[2]{\fun{Fun}(#1,#2)}
+\newcommand{\genOpens}[2]{\mathcal{O}_{#2}(#1)}
 \newcommand{\idempotents}[1]{\fun{Idempotent}(#1)}
 \newcommand{\identity}[1]{\fun{id}_{#1}}
 \newcommand{\img}[2]{#1^{\to}(#2)}
-- 
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(-)

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 9db5125330d293a9ea5eb09daf8198f7d5e18ca9 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 22 May 2024 16:56:50 +0200
Subject: Allow `\left` and `\right` everywhere

---
 source/Syntax/Token.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index 65c02ca..cb3f4cb 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -417,7 +417,7 @@ end = lexeme do
 
 -- | Parses an opening delimiter.
 opening :: Lexer (Located Token)
-opening = lexeme (paren <|> brace <|> group <|> bracket)
+opening = lexeme (group <|> optional (Char.string "\\left") *> (paren <|> brace <|> bracket))
     where
         brace = VisibleBraceL <$ lexeme (Char.string "\\{")
         group = InvisibleBraceL <$ lexeme (Char.char '{')
@@ -426,7 +426,7 @@ opening = lexeme (paren <|> brace <|> group <|> bracket)
 
 -- | Parses a closing delimiter.
 closing :: Lexer (Located Token)
-closing = lexeme (paren <|> brace <|> group <|> bracket)
+closing = lexeme (group <|> optional (Char.string "\\right") *> (paren <|> brace <|> bracket))
     where
         brace = VisibleBraceR <$ lexeme (Char.string "\\}")
         group = InvisibleBraceR <$ lexeme (Char.char '}')
-- 
cgit v1.2.3


From 477e03817e424c65b6249262804e147dd8e6ac7d Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 22 May 2024 16:57:07 +0200
Subject: Update defaulting for envvar

---
 source/Api.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/source/Api.hs b/source/Api.hs
index 421a8eb..95d5c8c 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -94,7 +94,7 @@ findAndReadFile path = do
     homeDir     <- getHomeDirectory
     currentDir  <- getCurrentDirectory
     userLib     <- (?? (homeDir </> "formalizations"))   <$> lookupEnv "NAPROCHE_LIB"
-    srcLib      <- (?? (homeDir </> "code/zf/library"))  <$> lookupEnv "NAPROCHE_SCR_LIB"
+    srcLib      <- (?? (homeDir </> "code/naproche-zf/library"))  <$> lookupEnv "NAPROCHE_SCR_LIB"
 
     existsCurrent     <- doesFileExist (currentDir </> path)
     existsUserLib     <- doesFileExist (userLib </> path)
-- 
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(-)

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 3e4e7afc69bf43b3b45bde346c92f267e9b15c39 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 22 May 2024 16:58:06 +0200
Subject: Add lemma `filter_setminus_in`

---
 library/set/filter.tex | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/library/set/filter.tex b/library/set/filter.tex
index 93309de..59b647f 100644
--- a/library/set/filter.tex
+++ b/library/set/filter.tex
@@ -38,6 +38,19 @@
     Follows by \cref{filter}.
 \end{proof}
 
+\begin{proposition}\label{filter_setminus_in}
+    Let $F$ be a filter on $S$.
+    Suppose $A\in F$.
+    Suppose $B\subseteq S$ and $S\setminus B\in F$.
+    Then $A\setminus B\in F$.
+\end{proposition}
+\begin{proof}
+    We have $A\subseteq S$.
+    Thus $A\setminus B = A\inter (S\setminus B)$ by \cref{setminus_eq_inter_complement}.
+    Now $S\setminus B\subseteq S$.
+    Follows by \cref{filter_inter_in_iff}.
+\end{proof}
+
 \subsection{Principal filters over a set}
 
 \begin{definition}\label{principalfilter}
@@ -72,8 +85,6 @@
     Suppose $X\notin\principalfilter{S}{A}$.
     Then $A\not\subseteq X$.
 \end{proposition}
-\begin{proof}
-\end{proof}
 
 \begin{definition}\label{maximalfilter}
     $F$ is a maximal filter on $S$ iff
-- 
cgit v1.2.3


From 342ac0ab2f01b0b98886a0b3db77917d86ded2dc Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 22 May 2024 20:17:33 +0200
Subject: Add filter lemmas

---
 library/set/filter.tex | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/library/set/filter.tex b/library/set/filter.tex
index 59b647f..e196b64 100644
--- a/library/set/filter.tex
+++ b/library/set/filter.tex
@@ -51,12 +51,24 @@
     Follows by \cref{filter_inter_in_iff}.
 \end{proof}
 
+\begin{proposition}\label{filter_in_iff_exists_subset}
+    Let $F$ be a filter on $S$.
+    Suppose $B\subseteq S$.
+    Then $B\in F$ iff there exists $A\subseteq B$ such that $A\in F$.
+\end{proposition}
+
+
 \subsection{Principal filters over a set}
 
 \begin{definition}\label{principalfilter}
     $\principalfilter{S}{A} = \{X\in\pow{S}\mid A\subseteq X\}$.
 \end{definition}
 
+\begin{proposition}\label{principalfilter_iff}
+    Suppose $A, B\subseteq S$.
+    Then $B\in\principalfilter{S}{A}$ iff $A\subseteq B$.
+\end{proposition}
+
 \begin{proposition}\label{principalfilter_is_filter}
     Suppose $A\subseteq S$.
     Suppose $A$ is inhabited.
-- 
cgit v1.2.3


From 9113b4fddb67e5a101e4a26ead3d1d1bf72664ce Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 22 May 2024 23:10:27 +0200
Subject: Update filter.tex

---
 library/set/filter.tex | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/library/set/filter.tex b/library/set/filter.tex
index e196b64..4537b81 100644
--- a/library/set/filter.tex
+++ b/library/set/filter.tex
@@ -69,6 +69,16 @@
     Then $B\in\principalfilter{S}{A}$ iff $A\subseteq B$.
 \end{proposition}
 
+\begin{proposition}\label{principalfilter_bottom}
+    Suppose $A\subseteq S$.
+    Then $A\in\principalfilter{S}{A}$.
+\end{proposition}
+
+\begin{proposition}\label{principalfilter_top}
+    Suppose $A\subseteq S$.
+    Then $S\in\principalfilter{S}{A}$.
+\end{proposition}
+
 \begin{proposition}\label{principalfilter_is_filter}
     Suppose $A\subseteq S$.
     Suppose $A$ is inhabited.
-- 
cgit v1.2.3


From 091da55df4de2d27697203fdddcdacd3c713b38c Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Thu, 23 May 2024 13:11:39 +0200
Subject: Update formatting

---
 library/set/powerset.tex | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/library/set/powerset.tex b/library/set/powerset.tex
index 80da4cb..7f30f68 100644
--- a/library/set/powerset.tex
+++ b/library/set/powerset.tex
@@ -6,8 +6,7 @@
     The powerset of $X$ denotes $\pow{X}$.
 \end{abbreviation}
 
-\begin{axiom}%
-\label{pow_iff}
+\begin{axiom}\label{pow_iff}
     $B\in\pow{A}$ iff $B\subseteq A$.
 \end{axiom}
 
@@ -76,7 +75,7 @@
 
 % LATER
 %\begin{proposition}\label{powerset_cons}
-%    Then $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$.
+%    $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$.
 %\end{proposition}
 
 \begin{proposition}\label{powerset_union_subseteq}
-- 
cgit v1.2.3


From a5deeef9c3214f0f2ccd90789f5344a88544d65b Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Sat, 25 May 2024 01:21:17 +0200
Subject: Prove `emptyset_open` to replace structure axiom

---
 library/set.tex                        |  6 ++----
 library/topology/topological-space.tex | 10 +++++++++-
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/library/set.tex b/library/set.tex
index e7e062f..fcd2642 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -131,8 +131,7 @@ which applies it to goals of the form “$A = B$” and  “$A \neq B$”.
     If $x$ and $y$ are empty, then $x = y$.
 \end{proposition}
 
-\begin{proposition}%
-\label{emptyset_subseteq}
+\begin{proposition}\label{emptyset_subseteq}
     For all $a$ we have $\emptyset \subseteq a$.
     % LATER $\emptyset$ is a subset of every set.
 \end{proposition}
@@ -266,8 +265,7 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     There exists $B\in C$ such that $A\in B$.
 \end{proof}
 
-\begin{proposition}%
-\label{unions_emptyset}
+\begin{proposition}\label{unions_emptyset}
     $\unions{\emptyset} = \emptyset$.
 \end{proposition}
 
diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index e467d48..2bbdf09 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -11,7 +11,6 @@
     such that
     \begin{enumerate}
         \item\label{opens_type} $\opens[X]$ is a family of subsets of $\carrier[X]$.
-        \item\label{emptyset_open} $\emptyset\in\opens[X]$.
         \item\label{carrier_open} $\carrier[X]\in\opens[X]$.
         \item\label{opens_inter} For all $A, B\in \opens[X]$ we have $A\inter B\in\opens[X]$.
         \item\label{opens_unions} For all $F\subseteq \opens[X]$ we have $\unions{F}\in\opens[X]$.
@@ -26,6 +25,15 @@
     $U$ is open in $X$ iff $U\in\opens[X]$.
 \end{abbreviation}
 
+\begin{proposition}\label{emptyset_open}
+    Let $X$ be a topological space.
+    Then $\emptyset$ is open in $X$.
+\end{proposition}
+\begin{proof}
+    We have $\unions{\emptyset} = \emptyset\subseteq\opens[X]$ by \cref{unions_emptyset,emptyset_subseteq}.
+    Follows by \cref{opens_unions}.
+\end{proof}
+
 \begin{proposition}\label{union_open}
     Let $X$ be a topological space.
     Suppose $A$, $B$ are open.
-- 
cgit v1.2.3


From 719bb860942fc1134ad4a4ae55db2713cd100f1a Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 28 May 2024 17:09:06 +0200
Subject: Pow closed under binary intersection

---
 library/set.tex          | 13 +++++--------
 library/set/powerset.tex | 11 +++++++++++
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/library/set.tex b/library/set.tex
index fcd2642..2fd18ea 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -551,14 +551,6 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Follows by set extensionality.
 \end{proof}
 
-\begin{proposition}\label{inter_subseteq_left}
-    $A\inter B\subseteq A$.
-\end{proposition}
-
-\begin{proposition}\label{inter_subseteq_right}
-    $A\inter B\subseteq B$.
-\end{proposition}
-
 \begin{proposition}\label{inter_emptyset}
     $A\inter\emptyset = \emptyset$.
 \end{proposition}
@@ -620,6 +612,11 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Follows by set extensionality.
 \end{proof}
 
+\begin{proposition}\label{inter_subseteq}
+    Suppose $A,B\subseteq C$.
+    Then $A\inter B\subseteq C$.
+\end{proposition}
+
 \begin{abbreviation}\label{closedunderinter}
     $T$ is closed under binary intersections
     iff for every $U,V\in T$ we have $U\inter V\in T$.
diff --git a/library/set/powerset.tex b/library/set/powerset.tex
index 7f30f68..ec5866f 100644
--- a/library/set/powerset.tex
+++ b/library/set/powerset.tex
@@ -46,6 +46,17 @@
     Follows by \cref{pow_iff,unions_subseteq_of_powerset_is_subseteq}.
 \end{proof}
 
+
+\begin{proposition}\label{inter_powerset}
+    Let $A,B\in\pow{C}$.
+    Then $A\inter B\in\pow{C}$.
+\end{proposition}
+\begin{proof}
+    We have $A,B\subseteq C$ by \cref{pow_iff}.
+    $A\inter B\subseteq C$ by \cref{inter_subseteq}.
+    Follows by \cref{pow_iff}.
+\end{proof}
+
 \begin{proposition}\label{unions_powerset}
     $\unions{\pow{A}} = A$.
 \end{proposition}
-- 
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(-)

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