From 29027c9d2cdbdfe59e48b5aa28eb2d32d1a4c1f7 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 24 Aug 2024 11:43:29 +0200
Subject: naproch sty extension

---
 library/topology/urysohn2.tex | 56 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 56 insertions(+)
 create mode 100644 library/topology/urysohn2.tex

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
new file mode 100644
index 0000000..8e5261e
--- /dev/null
+++ b/library/topology/urysohn2.tex
@@ -0,0 +1,56 @@
+\import{topology/topological-space.tex}
+\import{topology/separation.tex}
+\import{topology/continuous.tex}
+\import{topology/basis.tex}
+\import{numbers.tex}
+\import{function.tex}
+\import{set.tex}
+\import{cardinal.tex}
+\import{relation.tex}
+\import{relation/uniqueness.tex}
+\import{set/cons.tex}
+\import{set/powerset.tex}
+\import{set/fixpoint.tex}
+\import{set/product.tex}
+
+\section{Urysohns Lemma}
+
+
+
+\begin{abbreviation}\label{urysohnspace}
+    $X$ is a urysohn space iff
+    $X$ is a topological space and
+    for all $A,B \in \closeds{X}$ such that $A \inter B = \emptyset$
+    we have there exist $A',B' \in \opens[X]$
+    such that  $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$.    
+\end{abbreviation}
+
+
+\begin{definition}\label{intervalclosed}
+    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
+\end{definition}
+
+
+
+
+\begin{theorem}\label{urysohn}
+    Let $X$ be a urysohn space.
+    Suppose $A,B \in \closeds{X}$.
+    Suppose $A \inter B$ is empty.
+    Suppose $\carrier[X]$ is inhabited.
+    There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
+    and $f(A) = \zero$ and $f(B)= 1$ and $f$ is continuous.
+\end{theorem}
+\begin{proof}
+
+
+
+
+    
+    Contradiction.
+    
+\end{proof}
+
+\begin{theorem}\label{safe}
+    Contradiction.     
+\end{theorem}
-- 
cgit v1.2.3


From 30f7c63ce566c993816607f3368c357233693aae Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 27 Aug 2024 01:44:45 +0200
Subject: Experimental working commit, programm will compile But the Proof that
 the domain of the local function is not right. Also if in the definition of
 our local function we just use f(x) = x then we get a technical ambigus parse

---
 library/topology/urysohn2.tex |  8 ++++++--
 source/Checking.hs            | 13 +++++++------
 source/Meaning.hs             |  4 ++--
 source/Syntax/Abstract.hs     |  2 +-
 source/Syntax/Adapt.hs        |  4 ++--
 source/Syntax/Concrete.hs     | 13 ++++++++-----
 source/Syntax/Internal.hs     |  2 +-
 source/Syntax/Token.hs        | 17 +++++++++++++++--
 8 files changed, 42 insertions(+), 21 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 8e5261e..05ea180 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -44,10 +44,14 @@
 \begin{proof}
 
 
+    Define $f : X \to \reals$ such that  $f(x) = $
+    \begin{cases}
+        &(x + x) , x \in X
+        % & x ,x \in X    <- will result in technicly ambigus parse
+    \end{cases}
 
-
+    Trivial.
     
-    Contradiction.
     
 \end{proof}
 
diff --git a/source/Checking.hs b/source/Checking.hs
index 817c477..6d55ee1 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -543,7 +543,7 @@ checkProof = \case
         checkCalc calc
         assume [Asm (calcResult calc)]
         checkProof continue
-    DefineFunctionMathy funVar domVar ranVar argVar definitions continue -> do
+    DefineFunctionMathy funVar argVar domVar ranExpr definitions continue -> do
         -- We have f: X \to Y and x \mapsto ...  
         -- definition is a nonempty list of (expresssion e, formula phi)
         -- such that f(x) =  e if phi(x)
@@ -558,8 +558,8 @@ checkProof = \case
         setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` subdomainConjuctionLocalFunction argVar definitions )] -- check the disjunct union
         tellTasks
 
-        assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` TermVar ranVar)))] -- function f from \dom(f) \to \ran(f)
-        assume (functionSubdomianExpression funVar argVar definitions) --behavior on the subdomians
+        assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f)
+        assume (functionSubdomianExpression funVar argVar (NonEmpty.toList definitions)) --behavior on the subdomians
         setGoals goals
         checkProof continue
 
@@ -571,9 +571,10 @@ subdomainConjuctionLocalFunction argVar defintions =
     in TermVar argVar `IsElementOf` makeConjunction stmts
 
 
-functionSubdomianExpression :: VarSymbol -> VarSymbol -> NonEmpty (Term, Formula) -> [Asm]
-functionSubdomianExpression f a nxs = case nxs of
-    x:|xs -> singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a (NonEmpty.fromList xs)
+functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm]
+functionSubdomianExpression f a (x:xs) = singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a xs
+functionSubdomianExpression _ _ [] = []
+
     
 
 singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> (Term, Formula) -> Asm
diff --git a/source/Meaning.hs b/source/Meaning.hs
index ab98c9a..4a21fa3 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -606,9 +606,9 @@ glossProof = \case
             then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
             else error "mismatched variables in function definition."
     
-    Raw.DefineFunctionMathy funVar domVar ranVar funVar2 argVar definitions proof -> do
+    Raw.DefineFunctionMathy funVar domVar ranExpr funVar2 argVar definitions proof -> do
         if funVar == funVar2
-            then Sem.DefineFunctionMathy funVar domVar ranVar argVar <$> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
+            then Sem.DefineFunctionMathy funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
             else error "missmatched function names"
     Raw.Calc calc proof ->
         Sem.Calc <$> glossCalc calc <*> glossProof proof
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index 6372c87..13691e7 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -373,7 +373,7 @@ data Proof
     
     
     
-    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
+    | DefineFunctionMathy VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
     -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
     -- 
     deriving (Show, Eq, Ord)
diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index 3cff497..4b43bc6 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -34,8 +34,8 @@ scanChunk ltoks =
             matchOrErr struct "struct definition" pos
         Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ ->
             matchOrErr inductive "inductive definition" pos
-        Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ ->
-            matchOrErr signatureIntro "signature" pos
+        --Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ ->
+        --    matchOrErr signatureIntro "signature" pos
         _ -> []
 
 adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 69280c1..fe08fec 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -373,16 +373,16 @@ grammar lexicon@Lexicon{..} = mdo
     --     3 & \text{else}     
     -- \end{cases}
 
-    functionDefineCase <- rule $ (,) <$> expr <*> (_ampersand *> formula)
+    functionDefineCase <- rule $ (,) <$> (_ampersand *> (expr <|> exprVar )) <*> (_comma *> formula)
     defineFunctionMathy <-  rule    $ DefineFunctionMathy 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
                                     <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
-                                    <*> (_to *> varSymbol <* endMath <* _suchThat) 
+                                    <*> (_to *> expr <* endMath <* _suchThat) 
                                     -- <*> (_suchThat  *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula))))
                                     -- <*> (_suchThat  *> align (many1 (varSymbol <* exprApp <*  formula)))
-                                    <*> varSymbol <*> varSymbol <* symbol "="
-                                    <*> many1 functionDefineCase
-                                    <*> proof 
+                                    <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq <* endMath)
+                                    <*> cases (many1 functionDefineCase)
+                                    <*> proof
 
 
 
@@ -644,6 +644,9 @@ group body = token InvisibleBraceL *> body <* token InvisibleBraceR <?> "\"{...}
 align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
 align body = begin "align*" *> body <* end "align*"
 
+cases :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+cases body = begin "cases" *> body <* end "cases"
+
 
 maybeVarToken :: Located Token -> Maybe VarSymbol
 maybeVarToken ltok = case unLocated ltok of
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 0e3361d..7046161 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -436,7 +436,7 @@ data Proof
     | Define VarSymbol Term Proof
     | DefineFunction VarSymbol VarSymbol Term Term Proof
 
-    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Term, Formula)) Proof
+    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
 
 deriving instance Show Proof
 deriving instance Eq   Proof
diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index cb3f4cb..52da86a 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -189,6 +189,7 @@ toks = whitespace *> goNormal id <* eof
                 Nothing -> pure (f [])
                 Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:))
                 Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:))
+                Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:))
                 Just t -> goNormal (f . (t:))
         goText f = do
             r <- optional textToken
@@ -204,6 +205,7 @@ toks = whitespace *> goNormal id <* eof
                 Nothing -> pure (f [])
                 Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:))
                 Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:))
+                Just t@Located{unLocated = EndEnv "cases"} -> 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:))
@@ -219,12 +221,12 @@ toks = whitespace *> goNormal id <* eof
 -- | Parses a single normal mode token.
 tok :: Lexer (Located Token)
 tok =
-    word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command
+    word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> casesBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command
 
 -- | Parses a single math mode token.
 mathToken :: Lexer (Located Token)
 mathToken =
-    var <|> symbol <|> number <|> begin <|> alignEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command
+    var <|> symbol <|> number <|> begin <|> alignEnd <|> casesEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command
 
 beginText :: Lexer (Located Token)
 beginText = lexeme do
@@ -277,6 +279,11 @@ alignBegin = guardM isTextMode *> lexeme do
     setMathMode
     pure (BeginEnv "align*")
 
+casesBegin :: Lexer (Located Token)
+casesBegin = guardM isTextMode *> lexeme do
+    Char.string "\\begin{cases}"
+    setMathMode
+    pure (BeginEnv "cases")
 
 -- | Parses a single end math token.
 mathEnd :: Lexer (Located Token)
@@ -291,6 +298,12 @@ alignEnd = guardM isMathMode *> lexeme do
     setTextMode
     pure (EndEnv "align*")
 
+casesEnd :: Lexer (Located Token)
+casesEnd = guardM isMathMode *> lexeme do
+    Char.string "\\end{cases}"
+    setTextMode
+    pure (EndEnv "cases")
+
 
 -- | Parses a word. Words are returned casefolded, since we want to ignore their case later on.
 word :: Lexer (Located Token)
-- 
cgit v1.2.3


From 604d7a87b4c45ab13ef03e3c7a611ad4f9342f23 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 27 Aug 2024 02:13:29 +0200
Subject: ambigus parse fix. The proof goal must be changed, since now some
 could define a function with overlapping and worng subdomains

---
 library/topology/urysohn2.tex | 4 +++-
 source/Checking.hs            | 6 +++---
 source/Syntax/Concrete.hs     | 2 +-
 3 files changed, 7 insertions(+), 5 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 05ea180..f2f6ef3 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -46,7 +46,9 @@
 
     Define $f : X \to \reals$ such that  $f(x) = $
     \begin{cases}
-        &(x + x) , x \in X
+        &(x + x) &\text{if} x \in X
+        & x &\text{if} x \neq \zero
+        & \zero & \text{if} x = \zero
         % & x ,x \in X    <- will result in technicly ambigus parse
     \end{cases}
 
diff --git a/source/Checking.hs b/source/Checking.hs
index 6d55ee1..7362c93 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -564,11 +564,11 @@ checkProof = \case
         checkProof continue
 
 
--- | Makes a conjunction of all the subdomain statments
+-- | Makes a conjunction of all the subdomain statments <- this has to be checked!!!! TODO!!!!!!
 subdomainConjuctionLocalFunction :: VarSymbol -> NonEmpty (Term, Formula) -> Formula 
-subdomainConjuctionLocalFunction argVar defintions = 
+subdomainConjuctionLocalFunction _ defintions = 
     let stmts = [snd x | x <- NonEmpty.toList defintions]
-    in TermVar argVar `IsElementOf` makeConjunction stmts
+    in makeDisjunction stmts 
 
 
 functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm]
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index fe08fec..9d52995 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -373,7 +373,7 @@ grammar lexicon@Lexicon{..} = mdo
     --     3 & \text{else}     
     -- \end{cases}
 
-    functionDefineCase <- rule $ (,) <$> (_ampersand *> (expr <|> exprVar )) <*> (_comma *> formula)
+    functionDefineCase <- rule $ (,) <$> (_ampersand *> expr) <*> (_ampersand *> text _if *> formula)
     defineFunctionMathy <-  rule    $ DefineFunctionMathy 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
                                     <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
-- 
cgit v1.2.3


From 6acc5654f1702f2466006564a415546a3def16e3 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 27 Aug 2024 17:19:02 +0200
Subject: Feature Complete Finalised the proof output and goals. The Local
 Function definition now producces a Function f with the right domain and
 range, together with the rules presented in cases. Then proof goal of this
 local definition is set to for all x we have x is element of dom(f) if and
 only if x is in exactly one of the subdomains. This suffices as
 welldefindness check on f, besides the right range.

Further checks that should be implemented are the correct range of the function.
And optional subproof such that the presented goal can be check easily.
---
 library/topology/urysohn2.tex |  2 +-
 source/Checking.hs            | 37 ++++++++++++++++++++++++-------------
 source/Syntax/Internal.hs     | 10 ++++++++++
 3 files changed, 35 insertions(+), 14 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index f2f6ef3..ea49a6c 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -46,7 +46,7 @@
 
     Define $f : X \to \reals$ such that  $f(x) = $
     \begin{cases}
-        &(x + x) &\text{if} x \in X
+        &(x + k) &\text{if} x \in X \land k \in \naturals
         & x &\text{if} x \neq \zero
         & \zero & \text{if} x = \zero
         % & x ,x \in X    <- will result in technicly ambigus parse
diff --git a/source/Checking.hs b/source/Checking.hs
index 7362c93..b43923c 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -555,30 +555,41 @@ checkProof = \case
             ,Asm (relationNoun (TermVar funVar))]
 
         goals <- gets checkingGoals
-        setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` subdomainConjuctionLocalFunction argVar definitions )] -- check the disjunct union
+        setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` localFunctionGoal definitions)]
         tellTasks
 
         assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f)
-        assume (functionSubdomianExpression funVar argVar (NonEmpty.toList definitions)) --behavior on the subdomians
+        assume (functionSubdomianExpression funVar argVar domVar (NonEmpty.toList definitions)) --behavior on the subdomians
         setGoals goals
         checkProof continue
 
+-- |Creats the Goal \forall x. x \in dom{f} \iff (phi_{1}(x) \xor (\phi_{2}(x) \xor (... \xor (\phi_{n}) ..)))
+--  where the phi_{i} are the subdomain statments
+localFunctionGoal :: NonEmpty (Term,Formula) -> Formula
+localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs
 
--- | Makes a conjunction of all the subdomain statments <- this has to be checked!!!! TODO!!!!!!
-subdomainConjuctionLocalFunction :: VarSymbol -> NonEmpty (Term, Formula) -> Formula 
-subdomainConjuctionLocalFunction _ defintions = 
-    let stmts = [snd x | x <- NonEmpty.toList defintions]
-    in makeDisjunction stmts 
 
+-- We have our list of expr and forumlas, in this case normaly someone would write
+-- f(x) =  ....cases
+--      & (\frac{1}{k} \cdot x) &\text{if} x \in \[k, k+1\)
+--
+-- So therefore we have to check that all free varibels in lhs are free on rhs,
+-- since its an expression all varibals from the lhs has to be free on rhs. 
+--
+-- so we take (exp, frm) -> binding all free in exp 
+-- -> make forall [x, bound vars] x \in \dom(f) & frm => exp
 
-functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm]
-functionSubdomianExpression f a (x:xs) = singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a xs
-functionSubdomianExpression _ _ [] = []
 
-    
+functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm]
+functionSubdomianExpression f a d (x:xs) = singleFunctionSubdomianExpression f a d x : functionSubdomianExpression f a d xs
+functionSubdomianExpression _ _ _ [] = []
 
-singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> (Term, Formula) -> Asm
-singleFunctionSubdomianExpression funVar argVar x = Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` snd x) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` fst x)))
+singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> (Term, Formula) -> Asm
+singleFunctionSubdomianExpression funVar argVar domVar (expr, frm) = let
+    boundVar = Set.toList (freeVars expr) in
+    let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr)
+    in Asm def
+    
 
 
 checkCalc :: Calc -> Checking
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 7046161..e83126d 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -324,6 +324,16 @@ makeDisjunction = \case
     [] -> Bottom
     es -> List.foldl1' Or es
 
+makeIff :: [ExprOf a] -> ExprOf a
+makeIff = \case
+    [] -> Bottom
+    es -> List.foldl1' Iff es
+    
+makeXor :: [ExprOf a] -> ExprOf a
+makeXor = \case
+    [] -> Bottom
+    es -> List.foldl1' Xor es
+
 finiteSet :: NonEmpty (ExprOf a) -> ExprOf a
 finiteSet = foldr cons EmptySet
     where
-- 
cgit v1.2.3


From b8cc467735054bb3c38bf37b5e29877ba756c4b5 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 27 Aug 2024 20:20:46 +0200
Subject: working commit

---
 library/everything.tex        |  1 +
 library/topology/urysohn2.tex | 19 +++++++++++++++++++
 2 files changed, 20 insertions(+)

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

diff --git a/library/everything.tex b/library/everything.tex
index b966197..94dd6d8 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -30,6 +30,7 @@
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
 \import{numbers.tex}
+\import{topology/urysohn2.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index ea49a6c..a64fa7e 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -16,6 +16,22 @@
 \section{Urysohns Lemma}
 
 
+\begin{definition}\label{one_to_n_set}
+    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
+\end{definition}
+
+\begin{struct}\label{sequence}
+    A sequence $X$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\index$
+        \item $\indexset$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$.
+        \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$.
+    \end{enumerate}
+\end{struct}
 
 \begin{abbreviation}\label{urysohnspace}
     $X$ is a urysohn space iff
@@ -33,6 +49,7 @@
 
 
 
+
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -52,6 +69,8 @@
         % & x ,x \in X    <- will result in technicly ambigus parse
     \end{cases}
 
+
+    $U_1$
     Trivial.
     
     
-- 
cgit v1.2.3


From b64a56c6325e1c2f0876049fb2a7dda6c06dbe3a Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 28 Aug 2024 14:17:27 +0200
Subject: working commit

---
 library/topology/urysohn2.tex | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index a64fa7e..40a3615 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -46,7 +46,13 @@
     $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
 \end{definition}
 
-
+\begin{theorem}\label{urysohnsetinbeetween}
+    Let $X$ be a urysohn space.
+    Suppose $A,B \in \closeds{X}$.
+    Suppose $\closure{A}{X} \subseteq \interior{B}{X}$.
+    Suppose $\carrier[X]$ is inhabited.
+    There exist $U \subseteq \carrier[X]$ such that $U$ is closed in $X$ and $\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{B}{X}$.
+\end{theorem}
 
 
 
@@ -60,6 +66,10 @@
 \end{theorem}
 \begin{proof}
 
+    Let $H = \carrier[X] \setminus B$.
+    Let $P = \{x \in \pow{X} \mid x = A \lor x = H \lor (x \in \pow{X} \land (\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{H}{X}))\}$.
+
+
 
     Define $f : X \to \reals$ such that  $f(x) = $
     \begin{cases}
@@ -70,7 +80,7 @@
     \end{cases}
 
 
-    $U_1$
+    
     Trivial.
     
     
-- 
cgit v1.2.3


From 565db8eb643673f15c44bd8a8ac30debc9b388fd Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Thu, 29 Aug 2024 15:22:11 +0200
Subject: working commit

---
 library/topology/urysohn.tex  | 43 +++++++++++++++++++++++++++++++------------
 library/topology/urysohn2.tex | 30 ++++++++++++++++++++++--------
 2 files changed, 53 insertions(+), 20 deletions(-)

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

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index b8a5fa5..79d65dc 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -100,6 +100,14 @@ The first tept will be a formalisation of chain constructions.
 
 \subsection{staircase function}
 
+\begin{definition}\label{minimum}
+    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
+\end{definition}
+
+\begin{definition}\label{maximum}
+    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
+\end{definition}
+
 \begin{definition}\label{intervalclosed}
     $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
 \end{definition}
@@ -122,6 +130,9 @@ The first tept will be a formalisation of chain constructions.
         \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
         \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. 
         \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
+        \item \label{staircase_chain_indeset} There exist $n$ such that $\indexset[C] = \seq{\zero}{n}$.
+        \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexset[C]$ 
+            such that $n \neq \zero$ we have $f(\index[C](n) \setminus \index[C](n-1)) = \rfrac{n}{ \max{\indexset[C]} }$. 
     \end{enumerate}
 \end{struct}
 
@@ -311,13 +322,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{definition}\label{minimum}
-    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
-\end{definition}
 
-\begin{definition}\label{maximum}
-    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
-\end{definition}
 
 \begin{proposition}\label{urysohnchain_induction_step_existence}
     Let $X$ be a urysohn space.
@@ -562,6 +567,16 @@ The first tept will be a formalisation of chain constructions.
         Omitted.
     \end{subproof}
 
+    Let $\alpha = \carrier[X]$.
+    %Define $f : \alpha \to \naturals$ such that $f(x) =$
+    %\begin{cases}
+    %    & 1        & \text{if} x \in A \lor x \in B 
+    %    & k     & \text{if} \exists k \in \naturals 
+    %\end{cases}
+%
+    %We show that there exist $k \in \funs{\carrier[X]}{\reals}$ such that
+    %$k(x)$
+
     %For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$.
 
     We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$.
@@ -581,15 +596,19 @@ The first tept will be a formalisation of chain constructions.
 
     
     We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
-    and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ 
+    and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ such that $x \notin \index[\index[\zeta](m)](n-1)$ 
     we have $f(x) = \rfrac{n}{\pot(m)}$.
     \begin{subproof}
-        %   Fix $m \in \indexset[\zeta]$.
-        %   $\index[\zeta](m)$ is a urysohnchain in $X$.
-        %   
-        %   Follows by \cref{existence_of_staircase_function}.
+        Fix $m \in \indexset[\zeta]$.
+        $\index[\zeta](m)$ is a urysohnchain in $X$.
+        Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$
+        \begin{cases}
+            & 0  & \text{if} x \in A 
+            & 1 & \text{if} x \in B 
+            & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1)
+        \end{cases}
 
-        Omitted.
+        
     \end{subproof}
 
     
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 40a3615..71de210 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -68,18 +68,32 @@
 
     Let $H = \carrier[X] \setminus B$.
     Let $P = \{x \in \pow{X} \mid x = A \lor x = H \lor (x \in \pow{X} \land (\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{H}{X}))\}$.
+    Let $\eta = \carrier[X]$.
 
-
-
-    Define $f : X \to \reals$ such that  $f(x) = $
+    
+    % Provable 
+    % vvv
+    Define $F : \eta \to \reals$ such that $F(x) =$
     \begin{cases}
-        &(x + k) &\text{if} x \in X \land k \in \naturals
-        & x &\text{if} x \neq \zero
-        & \zero & \text{if} x = \zero
-        % & x ,x \in X    <- will result in technicly ambigus parse
+        & \zero                 &\text{if} x \in  A\\
+        & \rfrac{1}{1+1}    &\text{if} x \in  (\carrier[X] \setminus (A \union B))\\
+        & 1                 &\text{if} x \in  B
     \end{cases}
 
-
+    %Define $f : \naturals \to \pow{P}$ such that $f(x)=$
+    %\begin{cases}
+    %    & \emptyset             & \text{if} x = \zero \\
+    %    & \{A, H\}             & \text{if} x = 1  \\
+    %    & G                     & \text{if} x \in (\naturals \setminus \{1, \zero\}) \land  G = \{g \in \pow{P} \mid g \in f(n-1) \lor (g \notin f(n-1) \land g \in P) \}
+    %\end{cases}
+
+    Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$.
+    Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff 
+        $q = \zero \land S = A$ or $q = 1 \land S = H$ or 
+        for all $q_1, q_2, S_1, S_2$ 
+        such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ 
+        we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ 
+        and $q \mathrel{R} S$.
     
     Trivial.
     
-- 
cgit v1.2.3


From 26cf156763f71aaa9f638408ba4bffb85b886ab0 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 31 Aug 2024 18:02:42 +0200
Subject: working commit

---
 library/algebra/group.tex     |  10 +++
 library/topology/urysohn.tex  |   6 ++
 library/topology/urysohn2.tex | 157 +++++++++++++++++++++++++++++++++++-------
 3 files changed, 148 insertions(+), 25 deletions(-)

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

diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index a79bd2f..7de1051 100644
--- a/library/algebra/group.tex
+++ b/library/algebra/group.tex
@@ -80,3 +80,13 @@
 \begin{definition}\label{group_automorphism}
     Let $f$ be a function. $f$ is a group-automorphism iff $G$ is a group and $\dom{f}=G$ and $\ran{f}=G$. 
 \end{definition}
+
+\begin{definition}\label{trivial_group}
+    $G$ is the trivial group iff $G$ is a group and $\{\neutral[G]\}=G$.
+\end{definition}
+
+\begin{theorem}\label{trivial_implies_abelian}
+    Let $G$ be a group.
+    Suppose $G$ is the trivial group.
+    Then $G$ is an abelian group.
+\end{theorem}
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index e1fa924..17e2911 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -61,6 +61,11 @@ The first tept will be a formalisation of chain constructions.
     \end{enumerate}
 \end{struct}
 
+% Eine folge ist ein Funktion mit domain \subseteq Ordinal zahlen 
+
+
+
+
 \begin{definition}\label{cahin_of_subsets}
     $C$ is a chain of subsets iff
     $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$.
@@ -237,6 +242,7 @@ The first tept will be a formalisation of chain constructions.
     for all $x \in \carrier[X]$ we have $\{x\}$ is closed in $X$.
 \end{axiom}
 
+
 \begin{lemma}\label{urysohn_set_in_between}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 71de210..e963951 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -15,23 +15,35 @@
 
 \section{Urysohns Lemma}
 
+\begin{definition}\label{minimum}
+    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
+\end{definition}
+
+
+\begin{definition}\label{maximum}
+    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
+\end{definition}
+
+
+\begin{definition}\label{intervalclosed}
+    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
+\end{definition}
+
+
+\begin{definition}\label{intervalopen}
+    $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
+\end{definition}
+
 
 \begin{definition}\label{one_to_n_set}
     $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
 \end{definition}
 
-\begin{struct}\label{sequence}
-    A sequence $X$ is a onesorted structure equipped with
-    \begin{enumerate}
-        \item $\index$
-        \item $\indexset$
-    \end{enumerate}
-    such that
-    \begin{enumerate}
-        \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$.
-        \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$.
-    \end{enumerate}
-\end{struct}
+
+\begin{definition}\label{sequence}
+    $X$ is a sequence iff $X$ is a function and $\dom{f} \subseteq \naturals$.
+\end{definition}
+
 
 \begin{abbreviation}\label{urysohnspace}
     $X$ is a urysohn space iff
@@ -42,10 +54,66 @@
 \end{abbreviation}
 
 
-\begin{definition}\label{intervalclosed}
-    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
+\begin{abbreviation}\label{at}
+    $\at{f}{n} = f(n)$.
+\end{abbreviation}
+
+
+\begin{definition}\label{chain_of_subsets}
+    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$. 
+\end{definition}
+
+
+\begin{definition}\label{urysohnchain}%<-- zulässig
+    $X$ is a urysohnchain of $Y$ iff $X$ is a chain of subsets in $Y$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $\closure{\at{X}{n}}{Y} \subseteq \interior{\at{X}{m}}{Y}$.
+\end{definition}
+
+
+\begin{definition}\label{finer} %<-- verfeinerung 
+    $X$ is finer then $Y$ in $U$ iff for all $n \in \dom{X}$ we have $\at{X}{n} \in \ran{Y}$ and for all $m \in \dom{X}$ such that $n < m$ we have there exist $k \in \dom{Y}$ such that $ \closure{\at{X}{n}}{U} \subseteq \interior{\at{Y}{k}}{U} \subseteq \closure{\at{Y}{k}}{U} \subseteq \interior{\at{X}{m}}{U}$.
+\end{definition}
+
+
+\begin{definition}\label{sequence_of_reals}
+    $X$ is a sequence of reals iff $\ran{X} \subseteq \reals$.
+\end{definition}
+
+
+\begin{axiom}\label{abs_behavior1}
+    If $x \geq \zero$ then $\abs{x} = x$.
+\end{axiom}
+
+\begin{axiom}\label{abs_behavior2}
+    If $x < \zero$ then $\abs{x} = \neg{x}$.
+\end{axiom}
+
+\begin{definition}\label{realsminus}
+    $\realsminus = \{r \in \reals \mid r < \zero\}$.
 \end{definition}
 
+\begin{definition}\label{realsplus}
+    $\realsplus = \reals \setminus \realsminus$.
+\end{definition}
+
+\begin{definition}\label{epsilon_ball}
+    $\epsBall{x}{\epsilon} = \intervalopen{x-\epsilon}{x+\epsilon}$.
+\end{definition}
+
+\begin{definition}\label{pointwise_convergence}
+    $X$ converge to $x$ iff for all $\epsilon \in \realsplus$ there exist $N \in \dom{X}$ such that for all $n \in \dom{X}$ such that $n > N$ we have $\at{X}{n} \in \epsBall{x}{\epsilon}$.
+\end{definition}
+
+
+
+
+
+
+
+
+
+
+
+
 \begin{theorem}\label{urysohnsetinbeetween}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -55,7 +123,6 @@
 \end{theorem}
 
 
-
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -76,8 +143,8 @@
     Define $F : \eta \to \reals$ such that $F(x) =$
     \begin{cases}
         & \zero                 &\text{if} x \in  A\\
-        & \rfrac{1}{1+1}    &\text{if} x \in  (\carrier[X] \setminus (A \union B))\\
-        & 1                 &\text{if} x \in  B
+        & \rfrac{1}{1+1}        &\text{if} x \in  (\carrier[X] \setminus (A \union B))\\
+        & 1                     &\text{if} x \in  B
     \end{cases}
 
     %Define $f : \naturals \to \pow{P}$ such that $f(x)=$
@@ -87,19 +154,59 @@
     %    & G                     & \text{if} x \in (\naturals \setminus \{1, \zero\}) \land  G = \{g \in \pow{P} \mid g \in f(n-1) \lor (g \notin f(n-1) \land g \in P) \}
     %\end{cases}
 
-    Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$.
-    Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff 
-        $q = \zero \land S = A$ or $q = 1 \land S = H$ or 
-        for all $q_1, q_2, S_1, S_2$ 
-        such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ 
-        we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ 
-        and $q \mathrel{R} S$.
+    %Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$.
+    %Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff 
+    %    $q = \zero \land S = A$ or $q = 1 \land S = H$ or 
+    %    for all $q_1, q_2, S_1, S_2$ 
+    %    such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ 
+    %    we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ 
+    %    and $q \mathrel{R} S$.
     
-    Trivial.
     
     
+    %Let $J = \{(n,f) \mid n denots the cardinality of a urysohn chain on which f is a staircase function\}$.
+%
+    %Let $N = \naturals$.
+    %Define $j : N \to \funs{\carrier[X]}{\eals}$ such that $j(n) =$
+    %\begin{cases}
+    %    & f     &\text{if} n \in N \land \exist w \in J. J=(n,f)
+    %\end{cases}
+
+
+
+
+
+
+
+
+    
 \end{proof}
 
 \begin{theorem}\label{safe}
     Contradiction.     
 \end{theorem}
+
+
+
+
+%
+%Ideen:
+%Eine folge ist ein Funktion mit domain \subseteq Natürlichenzahlen. als predicat
+%
+%zulässig und verfeinerung von ketten als predicat definieren. 
+%
+%limits und punkt konvergenz als prädikat.
+%
+%
+%Vor dem Beweis vor dem eigentlichen Beweis.
+%die abgeleiteten Funktionen
+%
+%\derivedstiarcasefunction on A
+%
+%abbreviation: \at{f}{n} = f_{n}
+%
+%
+%TODO:
+%Reals ist ein topologischer Raum
+%
+
-- 
cgit v1.2.3


From 8cc2f8557d68c492cd0327f2f49051ff0a7b0f6a Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 31 Aug 2024 18:45:44 +0200
Subject: Contradiction in sequence False can be proven with iff_sequence,
 codom_of_emptyset_can_be_anything,sequence,
 emptyset_is_function_on_emptyset,id_dom,in_irrefl,
 suc_subseteq_implies_in,emptyset_subseteq

---
 library/topology/urysohn2.tex | 68 +++++++++++++++++--------------------------
 1 file changed, 26 insertions(+), 42 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index e963951..7f98bc2 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -104,8 +104,11 @@
 \end{definition}
 
 
-
-
+\begin{proposition}\label{iff_sequence}
+    Suppose $X$ is a function.
+    Suppose $\dom{X} \subseteq \naturals$.
+    Then $X$ is a sequence.
+\end{proposition}
 
 
 
@@ -121,6 +124,9 @@
     Suppose $\carrier[X]$ is inhabited.
     There exist $U \subseteq \carrier[X]$ such that $U$ is closed in $X$ and $\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{B}{X}$.
 \end{theorem}
+\begin{proof}
+    Omitted.
+\end{proof}
 
 
 \begin{theorem}\label{urysohn}
@@ -132,48 +138,26 @@
     and $f(A) = \zero$ and $f(B)= 1$ and $f$ is continuous.
 \end{theorem}
 \begin{proof}
-
-    Let $H = \carrier[X] \setminus B$.
-    Let $P = \{x \in \pow{X} \mid x = A \lor x = H \lor (x \in \pow{X} \land (\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{H}{X}))\}$.
-    Let $\eta = \carrier[X]$.
-
-    
-    % Provable 
-    % vvv
-    Define $F : \eta \to \reals$ such that $F(x) =$
+    Let $X' = \carrier[X]$.
+    Let $N = \{\zero, 1\}$.
+    $1 = \suc{\zero}$.
+    $1 \in \naturals$ and $\zero \in \naturals$.
+    $N \subseteq \naturals$.
+    Let $A' = (X' \setminus B)$.
+    $B \subseteq X'$ by \cref{powerset_elim,closeds}.
+    $A \subseteq X'$.
+    Therefore $A \subseteq A'$.
+    Define $U_0: N \to \{A, A'\}$ such that $U_0(n) =$
     \begin{cases}
-        & \zero                 &\text{if} x \in  A\\
-        & \rfrac{1}{1+1}        &\text{if} x \in  (\carrier[X] \setminus (A \union B))\\
-        & 1                     &\text{if} x \in  B
+        &A  &\text{if} n = \zero \\
+        &A' &\text{if} n = 1
     \end{cases}
-
-    %Define $f : \naturals \to \pow{P}$ such that $f(x)=$
-    %\begin{cases}
-    %    & \emptyset             & \text{if} x = \zero \\
-    %    & \{A, H\}             & \text{if} x = 1  \\
-    %    & G                     & \text{if} x \in (\naturals \setminus \{1, \zero\}) \land  G = \{g \in \pow{P} \mid g \in f(n-1) \lor (g \notin f(n-1) \land g \in P) \}
-    %\end{cases}
-
-    %Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$.
-    %Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff 
-    %    $q = \zero \land S = A$ or $q = 1 \land S = H$ or 
-    %    for all $q_1, q_2, S_1, S_2$ 
-    %    such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ 
-    %    we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ 
-    %    and $q \mathrel{R} S$.
-    
-    
-    
-    %Let $J = \{(n,f) \mid n denots the cardinality of a urysohn chain on which f is a staircase function\}$.
-%
-    %Let $N = \naturals$.
-    %Define $j : N \to \funs{\carrier[X]}{\eals}$ such that $j(n) =$
-    %\begin{cases}
-    %    & f     &\text{if} n \in N \land \exist w \in J. J=(n,f)
-    %\end{cases}
-
-
-
+    $U_0$ is a function.
+    $\dom{U_0} = N$.
+    $\dom{U_0} \subseteq \naturals$ by \cref{ran_converse}. 
+    $U_0$ is a sequence.
+    $U_0$ is a chain of subsets in $X'$.
+    $U_0$ is a urysohnchain of $X$.
 
 
 
-- 
cgit v1.2.3


From 36065f6a7fcc8f4d23b98be642c7fa7019ce2b79 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 2 Sep 2024 12:46:14 +0200
Subject: Corrected Contradiction. Contradiction was due to a misstake in the
 definition in sequence.

---
 library/topology/urysohn2.tex | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 7f98bc2..f70d679 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -41,7 +41,7 @@
 
 
 \begin{definition}\label{sequence}
-    $X$ is a sequence iff $X$ is a function and $\dom{f} \subseteq \naturals$.
+    $X$ is a sequence iff $X$ is a function and $\dom{X} \subseteq \naturals$.
 \end{definition}
 
 
@@ -169,6 +169,9 @@
 \begin{theorem}\label{safe}
     Contradiction.     
 \end{theorem}
+\begin{proof}
+    Follows by \cref{iff_sequence,codom_of_emptyset_can_be_anything,sequence,emptyset_is_function_on_emptyset,id_dom,in_irrefl,suc_subseteq_implies_in,emptyset_subseteq}. 
+\end{proof}
 
 
 
-- 
cgit v1.2.3


From d1d6ad98c26ffc392270665e8d0e4d2229984f82 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 2 Sep 2024 13:43:44 +0200
Subject: working commit

---
 library/topology/urysohn2.tex | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index f70d679..ad3f1d7 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -60,7 +60,7 @@
 
 
 \begin{definition}\label{chain_of_subsets}
-    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$. 
+    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$ and for all $m \in \dom{X}$ such that $m > n$ we have $\at{X}{n} \subseteq \at{X}{m}$. 
 \end{definition}
 
 
@@ -156,10 +156,20 @@
     $\dom{U_0} = N$.
     $\dom{U_0} \subseteq \naturals$ by \cref{ran_converse}. 
     $U_0$ is a sequence.
-    $U_0$ is a chain of subsets in $X'$.
+    We show that $U_0$ is a chain of subsets in $X$.
+    \begin{subproof}
+        We have $\dom{U_0} \subseteq \naturals$.
+        We have for all $n \in \dom{U_0}$ we have $\at{U_0}{n} \subseteq \carrier[X]$ by \cref{topological_prebasis_iff_covering_family,union_as_unions,union_absorb_subseteq_left,subset_transitive,setminus_subseteq}.
+        We have $\dom{U_0} = \{\zero, 1\}$.
+
+        It suffices to show that for all $n \in \dom{U_0}$ we have for all $m \in \dom{U_0}$ such that $m > n$ we have $\at{U_0}{n} \subseteq \at{U_0}{m}$.
+        
+        It suffices to show that $\at{U_0}{\zero} \subseteq \at{U_0}{1}$.
+        Follows by \cref{one_in_reals,order_reals_lemma0,upair_elim,reals_one_bigger_zero,reals_order,reals_axiom_zero_in_reals,subseteq_refl,apply}.
+    \end{subproof}
     $U_0$ is a urysohnchain of $X$.
 
-
+    %We are done with the first step, now we want to prove that we have U a sequence of these chain with U_0 the first chain.
 
 
 
@@ -169,9 +179,7 @@
 \begin{theorem}\label{safe}
     Contradiction.     
 \end{theorem}
-\begin{proof}
-    Follows by \cref{iff_sequence,codom_of_emptyset_can_be_anything,sequence,emptyset_is_function_on_emptyset,id_dom,in_irrefl,suc_subseteq_implies_in,emptyset_subseteq}. 
-\end{proof}
+
 
 
 
-- 
cgit v1.2.3


From 010b2ce53a4a5e693ced109eda38b167f3e284d7 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 2 Sep 2024 17:17:38 +0200
Subject: working commit

---
 library/topology/urysohn2.tex | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index ad3f1d7..c0b46c4 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -156,6 +156,7 @@
     $\dom{U_0} = N$.
     $\dom{U_0} \subseteq \naturals$ by \cref{ran_converse}. 
     $U_0$ is a sequence.
+    We have $1, \zero \in N$.
     We show that $U_0$ is a chain of subsets in $X$.
     \begin{subproof}
         We have $\dom{U_0} \subseteq \naturals$.
@@ -163,9 +164,24 @@
         We have $\dom{U_0} = \{\zero, 1\}$.
 
         It suffices to show that for all $n \in \dom{U_0}$ we have for all $m \in \dom{U_0}$ such that $m > n$ we have $\at{U_0}{n} \subseteq \at{U_0}{m}$.
+
+        Fix $n \in \dom{U_0}$.
+        Fix $m \in \dom{U_0}$.
+
+        \begin{byCase}
+            \caseOf{$n \neq \zero$.} 
+                Trivial.
+            \caseOf{$n = \zero$.} 
+                \begin{byCase}
+                    \caseOf{$m = \zero$.} 
+                        Trivial.
+                    \caseOf{$m \neq \zero$.}
+                        We have $A \subseteq A'$.
+                        We have $\at{U_0}{\zero} = A$ by assumption.
+                        We have $\at{U_0}{1}= A'$ by assumption.
+                \end{byCase}
+        \end{byCase}
         
-        It suffices to show that $\at{U_0}{\zero} \subseteq \at{U_0}{1}$.
-        Follows by \cref{one_in_reals,order_reals_lemma0,upair_elim,reals_one_bigger_zero,reals_order,reals_axiom_zero_in_reals,subseteq_refl,apply}.
     \end{subproof}
     $U_0$ is a urysohnchain of $X$.
 
-- 
cgit v1.2.3


From 6b45d0b6118cbfaf3406213601917394c364bfe2 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 3 Sep 2024 04:33:21 +0200
Subject: Finished induction begin

---
 library/topology/urysohn2.tex | 48 +++++++++++++++++++++++++++++++++++++++----
 1 file changed, 44 insertions(+), 4 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index c0b46c4..9991d21 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -68,11 +68,21 @@
     $X$ is a urysohnchain of $Y$ iff $X$ is a chain of subsets in $Y$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $\closure{\at{X}{n}}{Y} \subseteq \interior{\at{X}{m}}{Y}$.
 \end{definition}
 
+\begin{definition}\label{urysohn_finer_set}
+    $A$ is finer between $X$ to $Y$ in $U$ iff $\closure{X}{U} \subseteq \interior{A}{U}$ and $\closure{A}{U} \subseteq \interior{Y}{U}$.
+\end{definition}
 
 \begin{definition}\label{finer} %<-- verfeinerung 
-    $X$ is finer then $Y$ in $U$ iff for all $n \in \dom{X}$ we have $\at{X}{n} \in \ran{Y}$ and for all $m \in \dom{X}$ such that $n < m$ we have there exist $k \in \dom{Y}$ such that $ \closure{\at{X}{n}}{U} \subseteq \interior{\at{Y}{k}}{U} \subseteq \closure{\at{Y}{k}}{U} \subseteq \interior{\at{X}{m}}{U}$.
+    $Y$ is finer then $X$ in $U$ iff for all $n \in \dom{X}$ we have $\at{X}{n} \in \ran{Y}$ and for all $m \in \dom{X}$ such that $n < m$ we have there exist $k \in \dom{Y}$ such that $\at{Y}{k}$ is finer between $\at{X}{n}$ to $\at{X}{m}$ in $U$.
 \end{definition}
 
+\begin{definition}\label{follower_index}
+    $y$ follows $x$ in $I$ iff $x < y$ and $x,y \in I$ and for all $i \in I$ such that $x < i$ we have $y \leq i$.
+\end{definition}
+
+\begin{definition}\label{finer_smallest_step}
+    $Y$ is a minimal finer extention of $X$ in $U$ iff $Y$ is finer then $X$ in $U$ and for all $x_1,x_2 \in \dom{X}$ such that $x_1$ follows $x_2$ in $\dom{X}$ we have there exist $y \in \dom{Y}$ such that $y$ follows $x_1$ in $\dom{X}$ and $x_2$ follows $y$ in $\dom{X}$.
+\end{definition}
 
 \begin{definition}\label{sequence_of_reals}
     $X$ is a sequence of reals iff $\ran{X} \subseteq \reals$.
@@ -179,15 +189,45 @@
                         We have $A \subseteq A'$.
                         We have $\at{U_0}{\zero} = A$ by assumption.
                         We have $\at{U_0}{1}= A'$ by assumption.
+                        Follows by \cref{powerset_elim,emptyset_subseteq,union_as_unions,union_absorb_subseteq_left,subseteq_pow_unions,ran_converse,subseteq,subseteq_antisymmetric,suc_subseteq_intro,apply,powerset_emptyset,emptyset_is_ordinal,notin_emptyset,ordinal_elem_connex,omega_is_an_ordinal,prec_is_ordinal}.
                 \end{byCase}
         \end{byCase}
-        
     \end{subproof}
-    $U_0$ is a urysohnchain of $X$.
 
+    We show that $U_0$ is a urysohnchain of $X$.
+    \begin{subproof}
+        It suffices to show that for all $n \in \dom{U_0}$ we have for all $m \in \dom{U_0}$ such that $n < m$ we have $\closure{\at{U_0}{n}}{X} \subseteq \interior{\at{U_0}{m}}{X}$.
+        Fix $n \in \dom{U_0}$.
+        Fix $m \in \dom{U_0}$.
+        \begin{byCase}
+            \caseOf{$n \neq \zero$.} 
+                Follows by \cref{ran_converse,upair_iff,one_in_reals,order_reals_lemma0,reals_axiom_zero_in_reals,reals_one_bigger_zero,reals_order}.
+            \caseOf{$n = \zero$.} 
+                \begin{byCase}
+                    \caseOf{$m = \zero$.} 
+                        Trivial.
+                    \caseOf{$m \neq \zero$.}
+                        Follows by \cref{setminus_emptyset,setdifference_eq_intersection_with_complement,setminus_self,interior_carrier,complement_interior_eq_closure_complement,subseteq_refl,closure_interior_frontier_is_in_carrier,emptyset_subseteq,closure_is_minimal_closed_set,inter_lower_right,inter_lower_left,subseteq_transitive,interior_of_open,is_closed_in,closeds,union_absorb_subseteq_right,ordinal_suc_subseteq,ordinal_empty_or_emptyset_elem,union_absorb_subseteq_left,union_emptyset,topological_prebasis_iff_covering_family,inhabited,notin_emptyset,subseteq,union_as_unions,natural_number_is_ordinal}.
+                \end{byCase}
+        \end{byCase}
+    \end{subproof}
     %We are done with the first step, now we want to prove that we have U a sequence of these chain with U_0 the first chain.
 
-
+    We show that there exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
+    \begin{subproof}
+        $U_0$ is a urysohnchain of $X$.
+        We show that if $V$ is a urysohnchain of $X$ then there exist $V'$ such that $V'$ is a urysohnchain of $X$ and $V'$ is a minimal finer extention of $V$ in $X$.
+        \begin{subproof}
+            Omitted.
+        \end{subproof}
+        Let $N' = \naturals$.
+        Let $P = \{C \mid C \in \pow{\pow{X'}} \mid \text{$C$ is a urysohnchain of $X$}\}$.
+        Define $U : N' \to  P$ such that $U(n) =$
+        \begin{cases}
+            &U_0  &\text{if} n = \zero \\
+            &V     & \text{if}  \text{ $n = \suc{m}$ and $V$ is a minimal finer extention of $U(m)$ in $X$}.
+        \end{cases}
+    \end{subproof}
 
     
 \end{proof}
-- 
cgit v1.2.3


From c57360cf062805c86fed5d1f3f4adbf52c05f9ff Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 3 Sep 2024 05:45:37 +0200
Subject: working commit

---
 library/topology/urysohn2.tex | 44 +++++++++++++++++++++++++++++++------------
 1 file changed, 32 insertions(+), 12 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 9991d21..dbcfc53 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -120,6 +120,18 @@
     Then $X$ is a sequence.
 \end{proposition}
 
+\begin{definition}\label{higher_urysohn_chain}
+    $U$ is a lifted urysohnchain of $X$ iff $U$ is a sequence and $\dom{U} = \naturals$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
+\end{definition}
+
+\begin{definition}\label{staircase}
+    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and for all $x,n,m,k$ such that $k = \max{\dom{U}}$ and $n,m \in \dom{U}$ and $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ we have $f(x)= \rfrac{m}{k}$.
+\end{definition}
+
+\begin{definition}\label{staircase_sequence}
+    $f$ is staircase sequence of $U$ iff $f$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{f}$ and for all $n \in \dom{U}$ we have $\at{f}{n}$ is a staircase function adapted to $\at{U}{n}$ in $U$.
+\end{definition}
+
 
 
 
@@ -139,6 +151,23 @@
 \end{proof}
 
 
+\begin{theorem}\label{induction_on_urysohnchains}
+    Let $X$ be a urysohn space.
+    Suppose $U_0$ is a sequence.
+    Suppose $U_0$ is a chain of subsets in $X$.
+    Suppose $U_0$ is a urysohnchain of $X$.
+    There exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
+\end{theorem}
+\begin{proof}
+    $U_0$ is a urysohnchain of $X$.
+    It suffices to show that for all $V$ such that $V$ is a urysohnchain of $X$ there exist $V'$ such that $V'$ is a urysohnchain of $X$ and $V'$ is a minimal finer extention of $V$ in $X$.
+    
+\end{proof}
+
+
+
+
+
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -215,20 +244,11 @@
 
     We show that there exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
     \begin{subproof}
-        $U_0$ is a urysohnchain of $X$.
-        We show that if $V$ is a urysohnchain of $X$ then there exist $V'$ such that $V'$ is a urysohnchain of $X$ and $V'$ is a minimal finer extention of $V$ in $X$.
-        \begin{subproof}
-            Omitted.
-        \end{subproof}
-        Let $N' = \naturals$.
-        Let $P = \{C \mid C \in \pow{\pow{X'}} \mid \text{$C$ is a urysohnchain of $X$}\}$.
-        Define $U : N' \to  P$ such that $U(n) =$
-        \begin{cases}
-            &U_0  &\text{if} n = \zero \\
-            &V     & \text{if}  \text{ $n = \suc{m}$ and $V$ is a minimal finer extention of $U(m)$ in $X$}.
-        \end{cases}
+        Follows by \cref{chain_of_subsets,urysohnchain,induction_on_urysohnchains}.
     \end{subproof}
 
+
+
     
 \end{proof}
 
-- 
cgit v1.2.3


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/numbers.tex                         |  40 +++++++++++
 library/topology/real-topological-space.tex |  26 +++++++
 library/topology/urysohn2.tex               | 108 +++++++++++++++-------------
 3 files changed, 125 insertions(+), 49 deletions(-)
 create mode 100644 library/topology/real-topological-space.tex

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

diff --git a/library/numbers.tex b/library/numbers.tex
index f7f6c2c..cb3d5cf 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -747,9 +747,49 @@ Laws of the order on the reals
     $x$ is the supremum of $X$ iff $x$ is a greatest lower bound of $X$.
 \end{definition}
 
+\begin{definition}\label{minimum}
+    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
+\end{definition}
+
+
+\begin{definition}\label{maximum}
+    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
+\end{definition}
+
+
+\begin{definition}\label{intervalclosed}
+    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
+\end{definition}
+
+
+\begin{definition}\label{intervalopen}
+    $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
+\end{definition}
 
 
+\begin{definition}\label{m_to_n_set}
+    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
+\end{definition}
+
+\begin{axiom}\label{abs_behavior1}
+    If $x \geq \zero$ then $\abs{x} = x$.
+\end{axiom}
+
+\begin{axiom}\label{abs_behavior2}
+    If $x < \zero$ then $\abs{x} = \neg{x}$.
+\end{axiom}
 
+\begin{definition}\label{realsminus}
+    $\realsminus = \{r \in \reals \mid r < \zero\}$.
+\end{definition}
+
+\begin{definition}\label{realsplus}
+    $\realsplus = \reals \setminus \realsminus$.
+\end{definition}
+
+\begin{definition}\label{epsilon_ball}
+    $\epsBall{x}{\epsilon} = \intervalopen{x-\epsilon}{x+\epsilon}$.
+\end{definition}
 
 
 
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
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index dbcfc53..a3f3ea4 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -12,32 +12,11 @@
 \import{set/powerset.tex}
 \import{set/fixpoint.tex}
 \import{set/product.tex}
+\import{topology/real-topological-space.tex}
 
 \section{Urysohns Lemma}
 
-\begin{definition}\label{minimum}
-    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
-\end{definition}
-
-
-\begin{definition}\label{maximum}
-    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
-\end{definition}
-
-
-\begin{definition}\label{intervalclosed}
-    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
-\end{definition}
-
-
-\begin{definition}\label{intervalopen}
-    $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
-\end{definition}
-
 
-\begin{definition}\label{one_to_n_set}
-    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
-\end{definition}
 
 
 \begin{definition}\label{sequence}
@@ -89,26 +68,6 @@
 \end{definition}
 
 
-\begin{axiom}\label{abs_behavior1}
-    If $x \geq \zero$ then $\abs{x} = x$.
-\end{axiom}
-
-\begin{axiom}\label{abs_behavior2}
-    If $x < \zero$ then $\abs{x} = \neg{x}$.
-\end{axiom}
-
-\begin{definition}\label{realsminus}
-    $\realsminus = \{r \in \reals \mid r < \zero\}$.
-\end{definition}
-
-\begin{definition}\label{realsplus}
-    $\realsplus = \reals \setminus \realsminus$.
-\end{definition}
-
-\begin{definition}\label{epsilon_ball}
-    $\epsBall{x}{\epsilon} = \intervalopen{x-\epsilon}{x+\epsilon}$.
-\end{definition}
-
 \begin{definition}\label{pointwise_convergence}
     $X$ converge to $x$ iff for all $\epsilon \in \realsplus$ there exist $N \in \dom{X}$ such that for all $n \in \dom{X}$ such that $n > N$ we have $\at{X}{n} \in \epsBall{x}{\epsilon}$.
 \end{definition}
@@ -120,10 +79,61 @@
     Then $X$ is a sequence.
 \end{proposition}
 
-\begin{definition}\label{higher_urysohn_chain}
+\begin{definition}\label{lifted_urysohn_chain}
     $U$ is a lifted urysohnchain of $X$ iff $U$ is a sequence and $\dom{U} = \naturals$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
 \end{definition}
 
+\begin{definition}\label{normal_ordered_urysohnchain}
+    $U$ is normal ordered iff there exist $n \in \naturals$ such that $\dom{U} = \seq{\zero}{n}$.
+\end{definition}
+
+\begin{definition}\label{bijection_of_urysohnchains}
+    $f$ is consistent on $X$ to $Y$ iff $f$ is a bijection from $\dom{X}$ to $\dom{Y}$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $f(n) < f(m)$.
+\end{definition}
+
+\begin{proposition}\label{naturals_in_transitive}
+    $\naturals$ is a \in-transitive set.
+\end{proposition}
+
+\begin{proposition}\label{naturals_elem_in_transitive}
+    If $n \in \naturals$ then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
+    %If $n$ is a natural number then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
+    
+\end{proposition}
+
+\begin{proposition}\label{seq_zero_to_n_isomorph_to_n}
+    For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
+\end{proposition}
+\begin{proof} [Proof by \in-induction on $n$]
+    Assume $n \in \naturals$.
+    %Assume $n$ is a natural number.
+    %We show that $\seq{\zero}{\zero}$ has cardinality $1$.
+    %\begin{subproof}
+    %    It suffices to show that $1 = \seq{\zero}{\zero}$.
+    %    Follows by set extensionality.
+    %\end{subproof}
+    %For all $n \in \naturals$ we have either $n = \zero$ or there exist $m \in \naturals$ such that $n = \suc{m}$.
+    %For all $n \in \naturals$ we have either $n = \zero$ or $\zero \in n$.
+    %We show that if $\seq{\zero}{n}$ has cardinality $\suc{n}$ then $\seq{\zero}{\suc{n}}$ has cardinality $\suc{\suc{n}}$.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+\end{proof}
+
+\begin{proposition}\label{existence_normal_ordered_urysohn}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain of $X$.
+    Suppose $\dom{U}$ is finite.
+    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $X$ to $Y$ and $V$ is normal ordered.
+\end{proposition}
+\begin{proof}
+    Take $k$ such that $\dom{U}$ has cardinality $k$ by \cref{ran_converse,cardinality,finite}.
+    There exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$.
+
+
+\end{proof}
+
+
 \begin{definition}\label{staircase}
     $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and for all $x,n,m,k$ such that $k = \max{\dom{U}}$ and $n,m \in \dom{U}$ and $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ we have $f(x)= \rfrac{m}{k}$.
 \end{definition}
@@ -136,9 +146,6 @@
 
 
 
-
-
-
 \begin{theorem}\label{urysohnsetinbeetween}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -159,9 +166,9 @@
     There exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
 \end{theorem}
 \begin{proof}
-    $U_0$ is a urysohnchain of $X$.
-    It suffices to show that for all $V$ such that $V$ is a urysohnchain of $X$ there exist $V'$ such that $V'$ is a urysohnchain of $X$ and $V'$ is a minimal finer extention of $V$ in $X$.
-    
+    %$U_0$ is a urysohnchain of $X$.
+    %It suffices to show that for all $V$ such that $V$ is a urysohnchain of $X$ there exist $V'$ such that $V'$ is a urysohnchain of $X$ and $V'$ is a minimal finer extention of $V$ in $X$.
+    Omitted.
 \end{proof}
 
 
@@ -246,6 +253,9 @@
     \begin{subproof}
         Follows by \cref{chain_of_subsets,urysohnchain,induction_on_urysohnchains}.
     \end{subproof}
+    Take $U$ such that $U$ is a lifted urysohnchain of $X$ and $\at{U}{\zero} = U_0$.
+
+
 
 
 
-- 
cgit v1.2.3


From 22e9ebe72c349514a1ee0ed37772ca8168eaf658 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 4 Sep 2024 17:02:07 +0200
Subject: working commit

---
 library/topology/urysohn2.tex | 56 +++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 54 insertions(+), 2 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index a3f3ea4..d08d507 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -98,20 +98,68 @@
 \begin{proposition}\label{naturals_elem_in_transitive}
     If $n \in \naturals$ then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
     %If $n$ is a natural number then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
-    
 \end{proposition}
 
-\begin{proposition}\label{seq_zero_to_n_isomorph_to_n}
+\begin{proposition}\label{zero_is_in_minimal}
+    $\zero$ is an \in-minimal element of $\naturals$.
+\end{proposition}
+
+\begin{proposition}\label{seq_zero_to_n_isomorph_to_suc_n}
     For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
 \end{proposition}
 \begin{proof} [Proof by \in-induction on $n$]
     Assume $n \in \naturals$.
+    For all $m \in n$ we have $m \in \naturals$.
+    \begin{byCase}
+        \caseOf{$n = \zero$.}
+            It suffices to show that $1 = \seq{\zero}{\zero}$.
+            Follows by set extensionality.
+        \caseOf{$n \neq \zero$.}
+            Take $k$ such that $k \in \naturals$ and $\suc{k} = n$.
+            Then $k \in n$.
+            Therefore $\seq{\zero}{k}$ has cardinality $\suc{k}$.
+            Now $\seq{\zero}{k}$ has cardinality $n$.
+            Take $f$ such that $f$ is a bijection from $n$ to $\seq{\zero}{k}$.
+            We have $\suc{n} = n \union \{n\}$.
+            We show that $\seq{\zero}{n} = \seq{\zero}{k} \union \{\suc{k}\}$.
+            \begin{subproof}
+                We show that $\seq{\zero}{n} \subseteq \seq{\zero}{k} \union \{\suc{k}\}$.
+                \begin{subproof}
+                    Omitted.
+                \end{subproof}
+                We show that $\seq{\zero}{k} \union \{\suc{k}\} \subseteq \seq{\zero}{n}$.
+                \begin{subproof}
+                    Omitted.
+                \end{subproof}
+                %$\seq{\zero}{k} \subseteq \seq{\zero}{n}$.
+            \end{subproof}
+            We have $\{n\} \notin n$.
+            We have $n \notmeets \{n\}$.
+            Let $X = \suc{n}$.
+            Let $Y = \seq{\zero}{n}$.
+            Define $F : X \to Y$ such that $F(x) =$
+            \begin{cases}
+                &f(x) &\text{if} x \in n\\
+                &\suc{k} &\text{if} x \in \{n\} 
+            \end{cases}
+
+    \end{byCase}
+
     %Assume $n$ is a natural number.
     %We show that $\seq{\zero}{\zero}$ has cardinality $1$.
     %\begin{subproof}
     %    It suffices to show that $1 = \seq{\zero}{\zero}$.
     %    Follows by set extensionality.
     %\end{subproof}
+    %It suffices to show that if $n \neq \zero$ then $\seq{\zero}{n}$ has cardinality $\suc{n}$.
+    %We show that for all $m \in \naturals$ such that $m \neq \zero$ we have $\seq{\zero}{m}$ has cardinality $\suc{m}$.
+    %\begin{subproof}
+    %    Fix $m \in \naturals$.
+    %    Take $k$ such that $k \in \naturals$ and $\suc{k} = m$.
+    %    Then $k \in m$.
+    %\end{subproof}
+    
+    
     %For all $n \in \naturals$ we have either $n = \zero$ or there exist $m \in \naturals$ such that $n = \suc{m}$.
     %For all $n \in \naturals$ we have either $n = \zero$ or $\zero \in n$.
     %We show that if $\seq{\zero}{n}$ has cardinality $\suc{n}$ then $\seq{\zero}{\suc{n}}$ has cardinality $\suc{\suc{n}}$.
@@ -120,6 +168,10 @@
     %\end{subproof}
 \end{proof}
 
+%\begin{proposition}\label{seq_zero_to_n_isomorph_to_suc_n}
+%    For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
+%\end{proposition}
+%
 \begin{proposition}\label{existence_normal_ordered_urysohn}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain of $X$.
-- 
cgit v1.2.3


From e1d55f672b063f9347c0c9718ae5cdca9a370dba Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Thu, 5 Sep 2024 01:17:16 +0200
Subject: working commit

---
 library/topology/urysohn2.tex | 75 ++++++++++++++++++++++++++++---------------
 1 file changed, 49 insertions(+), 26 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index d08d507..93819dc 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -104,11 +104,31 @@
     $\zero$ is an \in-minimal element of $\naturals$.
 \end{proposition}
 
-\begin{proposition}\label{seq_zero_to_n_isomorph_to_suc_n}
-    For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
+\begin{proposition}\label{naturals_leq}
+    For all $n \in \naturals$ we have $\zero \leq n$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{naturals_leq_on_suc}
+    For all $n,m \in \naturals$ such that $m < \suc{n}$ we have $m \leq n$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{x_in_seq_iff}
+    Suppose $n,m,x \in \naturals$.
+    $x \in \seq{n}{m}$ iff $n \leq x \leq m$.
+\end{proposition}
+
+\begin{proposition}\label{seq_zero_to_n_eq_to_suc_n}
+    For all $n \in \naturals$ we have $\seq{\zero}{n} = \suc{n}$.
 \end{proposition}
 \begin{proof} [Proof by \in-induction on $n$]
     Assume $n \in \naturals$.
+    $n \in \naturals$.
     For all $m \in n$ we have $m \in \naturals$.
     \begin{byCase}
         \caseOf{$n = \zero$.}
@@ -117,32 +137,35 @@
         \caseOf{$n \neq \zero$.}
             Take $k$ such that $k \in \naturals$ and $\suc{k} = n$.
             Then $k \in n$.
-            Therefore $\seq{\zero}{k}$ has cardinality $\suc{k}$.
-            Now $\seq{\zero}{k}$ has cardinality $n$.
-            Take $f$ such that $f$ is a bijection from $n$ to $\seq{\zero}{k}$.
-            We have $\suc{n} = n \union \{n\}$.
-            We show that $\seq{\zero}{n} = \seq{\zero}{k} \union \{\suc{k}\}$.
+            Therefore $\seq{\zero}{k} = \suc{k}$.
+            We show that $\seq{\zero}{n} = \seq{\zero}{k} \union \{n\}$.
             \begin{subproof}
-                We show that $\seq{\zero}{n} \subseteq \seq{\zero}{k} \union \{\suc{k}\}$.
+                We show that $\seq{\zero}{n} \subseteq \seq{\zero}{k} \union \{n\}$.
                 \begin{subproof}
-                    Omitted.
+                    It suffices to show that for all $x \in \seq{\zero}{n}$ we have $x \in \seq{\zero}{k} \union \{n\}$.
+                    $n \in \naturals$.
+                    $\zero \leq n$.
+                    $n \leq n$.
+                    We have $n \in \seq{\zero}{n}$.
+                    Therefore $\seq{\zero}{n}$ is inhabited.
+                    Take $x$ such that $x \in \seq{\zero}{n}$.
+                    Therefore $\zero \leq x \leq n$.
+                    $x = n$ or $x < n$.
+                    Then either $x = n$ or $x \leq k$.
+                    Therefore $x \in \seq{\zero}{k}$ or $x = n$.
+                    Follows by \cref{reals_order,natural_number_is_ordinal,ordinal_empty_or_emptyset_elem,naturals_leq_on_suc,reals_axiom_zero_in_reals,naturals_subseteq_reals,subseteq,union_intro_left,naturals_inductive_set,m_to_n_set,x_in_seq_iff,union_intro_right,singleton_intro}.
                 \end{subproof}
-                We show that $\seq{\zero}{k} \union \{\suc{k}\} \subseteq \seq{\zero}{n}$.
+                We show that $\seq{\zero}{k} \union \{n\} \subseteq \seq{\zero}{n}$.
                 \begin{subproof}
-                    Omitted.
+                    $k \leq n$ by \cref{naturals_subseteq_reals,suc_eq_plus_one,plus_one_order,subseteq}.
+                    $k \in n$.
+                    $\seq{\zero}{k} = k$ by \cref{}.
+                    We have $\seq{\zero}{k} \subseteq \seq{\zero}{n}$.
+                    $n \in \seq{\zero}{n}$.
                 \end{subproof}
-                %$\seq{\zero}{k} \subseteq \seq{\zero}{n}$.
+                Trivial.
             \end{subproof}
-            We have $\{n\} \notin n$.
-            We have $n \notmeets \{n\}$.
-            Let $X = \suc{n}$.
-            Let $Y = \seq{\zero}{n}$.
-            Define $F : X \to Y$ such that $F(x) =$
-            \begin{cases}
-                &f(x) &\text{if} x \in n\\
-                &\suc{k} &\text{if} x \in \{n\} 
-            \end{cases}
-
+            We have $\suc{n} = n \union \{n\}$.
     \end{byCase}
 
     %Assume $n$ is a natural number.
@@ -168,10 +191,10 @@
     %\end{subproof}
 \end{proof}
 
-%\begin{proposition}\label{seq_zero_to_n_isomorph_to_suc_n}
-%    For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
-%\end{proposition}
-%
+\begin{proposition}\label{seq_zero_to_n_isomorph_to_suc_n}
+    For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
+\end{proposition}
+
 \begin{proposition}\label{existence_normal_ordered_urysohn}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain of $X$.
-- 
cgit v1.2.3


From 12f360a500d5edddf83afa121a5a08b6a6408815 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Thu, 5 Sep 2024 16:13:04 +0200
Subject: Precondtion failed in line 161 urysohn2.tex

Error:
zf: Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: TermSep (NamedVar "n") (TermSymbol (SymbolMixfix [Just (Command "naturals")]) []) (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "rless"))) [TermSymbol (SymbolInteger 1) [],TermVar (B ())]))
CallStack (from HasCallStack):
  error, called at source/Encoding.hs:89:13 in zf-0.3.0.0-3mIpbM9y9fK3yXjxxoLDb2:Encoding
---
 library/topology/urysohn2.tex | 138 ++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 133 insertions(+), 5 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 93819dc..396255e 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -100,17 +100,129 @@
     %If $n$ is a natural number then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
 \end{proposition}
 
+\begin{proposition}\label{natural_number_is_ordinal_for_all}
+    For all $n \in \naturals$ we have $n$ is a ordinal.
+\end{proposition}
+
 \begin{proposition}\label{zero_is_in_minimal}
     $\zero$ is an \in-minimal element of $\naturals$.
 \end{proposition}
 
-\begin{proposition}\label{naturals_leq}
-    For all $n \in \naturals$ we have $\zero \leq n$.
+\begin{proposition}\label{natural_rless_eq_precedes}
+    For all $n,m \in \naturals$ we have $n \precedes m$ iff $n \in m$.
+\end{proposition}
+
+\begin{proposition}\label{naturals_precedes_suc}
+    For all $n \in \naturals$ we have $n \precedes \suc{n}$.
+\end{proposition}
+
+\begin{proposition}\label{zero_is_empty}
+    There exists no $x$ such that $x \in \zero$.
+\end{proposition}
+
+\begin{proposition}\label{one_is_positiv}
+    $1$ is positiv.
+\end{proposition}
+
+\begin{proposition}\label{suc_of_positive_is_positive}
+    For all $n \in \naturals$ such that $n$ is positiv we have $\suc{n}$ is positiv.
+\end{proposition}
+
+\begin{proposition}\label{naturals_are_positiv_besides_zero}
+    For all $n \in \naturals$ such that $n \neq \zero$ we have $n$ is positiv.
+\end{proposition}
+\begin{proof}[Proof by \in-induction on $n$]
+    Assume $n \in \naturals$.
+    \begin{byCase}
+        \caseOf{$n = \zero$.} Trivial.
+        \caseOf{$n \neq \zero$.}
+            Take $k \in \naturals$ such that $\suc{k} = n$.
+    \end{byCase}
+\end{proof}
+
+
+
+\begin{proposition}\label{naturals_sum_eq_zero}
+    For all $n,m \in \naturals$ we have if $n+m = \zero$ then $n = m = \zero$.
 \end{proposition}
 \begin{proof}
     Omitted.
 \end{proof}
 
+\begin{proposition}\label{no_natural_between_n_and_suc_n}
+    For all $n,m \in \naturals$ we have not $n < m < \suc{n}$.
+\end{proposition}
+
+\begin{proposition}\label{naturals_rless_existence_of_lesser_natural}
+    For all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ there exist $k \in \naturals$ such that $m + k = n$.
+\end{proposition}
+\begin{proof}[Proof by \in-induction on $n$]
+    Assume $n \in \naturals$.
+    We show that $\naturals = (\{\zero, 1\} \union \{n \in \naturals \mid n > 1\})$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+    \begin{byCase}
+        \caseOf{$n = \zero$.} 
+            
+            We show that for all $m \in \naturals$ such that $m < n$ we have there exist $k \in \naturals$ such that $m + k = n$.
+            \begin{subproof}[Proof by \in-induction on $m$]
+                Assume $m \in \naturals$.
+                \begin{byCase}
+                    \caseOf{$m = \zero$.}
+                        Trivial.
+                    \caseOf{$m \neq \zero$.}
+                        Trivial.
+                \end{byCase}
+            \end{subproof}
+        \caseOf{$n = 1$.}
+            Fix $m$.
+            For all $l \in \naturals$ we have If $l < 1$ then $l = \zero$.
+            Then $\zero + 1 = 1$.
+        \caseOf{$n > 1$.} 
+            Take $l \in \naturals$ such that $\suc{l} = n$.
+            Omitted.
+    \end{byCase}
+\end{proof}
+
+
+\begin{proposition}\label{rless_eq_in_for_naturals}
+    For all $n,m \in \naturals$ such that $n < m$ we have $n \in m$. 
+\end{proposition}
+\begin{proof}
+    We show that for all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ we have $m \in n$.
+    \begin{subproof}[Proof by \in-induction on $n$]
+        Assume $n \in \naturals$.
+        We show that for all $m \in \naturals$ such that$m < n$ we have $m \in n$.
+        \begin{subproof}[Proof by \in-induction on $m$]
+            Assume $m \in \naturals$.
+            %\begin{byCase}
+            %    
+            %\end{byCase}
+        \end{subproof}
+    \end{subproof}
+    
+    %Fix $n \in \naturals$.
+
+    %\begin{byCase}
+    %    \caseOf{$n = \zero$.}
+    %        For all $k \in \naturals$ we have $k = \zero$ or $\zero < k$.
+    %        
+    %    \caseOf{$n \neq \zero$.}
+    %        Fix $m \in \naturals$.
+    %        It suffices to show that $m \in n$.
+    %\end{byCase}
+    
+\end{proof}
+
+
+
+\begin{proposition}\label{naturals_leq}
+    For all $n \in \naturals$ we have $\zero \leq n$.
+\end{proposition}
+
+
+
 \begin{proposition}\label{naturals_leq_on_suc}
     For all $n,m \in \naturals$ such that $m < \suc{n}$ we have $m \leq n$.
 \end{proposition}
@@ -157,11 +269,27 @@
                 \end{subproof}
                 We show that $\seq{\zero}{k} \union \{n\} \subseteq \seq{\zero}{n}$.
                 \begin{subproof}
+                    It suffices to show that for all $x \in \seq{\zero}{k} \union \{n\}$ we have $x \in \seq{\zero}{n}$.
                     $k \leq n$ by \cref{naturals_subseteq_reals,suc_eq_plus_one,plus_one_order,subseteq}.
                     $k \in n$.
-                    $\seq{\zero}{k} = k$ by \cref{}.
-                    We have $\seq{\zero}{k} \subseteq \seq{\zero}{n}$.
-                    $n \in \seq{\zero}{n}$.
+                    $\seq{\zero}{k} = \suc{k}$ by assumption.            
+                    $n \in \naturals$.
+                    $\zero \leq n$.
+                    $n \leq n$.
+                    We have $n \in \seq{\zero}{n}$.
+                    Therefore $\seq{\zero}{n}$ is inhabited.
+                    Take $x$ such that $x \in \seq{\zero}{n}$.
+                    Therefore $\zero \leq x \leq n$.
+                    $x = n$ or $x < n$.
+                    Then either $x = n$ or $x \leq k$.
+                    Therefore $x \in \seq{\zero}{k}$ or $x = n$.
+                    Fix $x$.
+                    \begin{byCase}
+                        \caseOf{$x \in \seq{\zero}{k}$.}
+                            Trivial.
+                        \caseOf{$x = n$.}
+                            It suffices to show that $n \in \seq{\zero}{n}$.
+                    \end{byCase}
                 \end{subproof}
                 Trivial.
             \end{subproof}
-- 
cgit v1.2.3


From b298295ac002785672a8b16dd09f9692d73f7a80 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 15 Sep 2024 15:07:36 +0200
Subject: Issue at Fixing.

In Line 49 in real-topological-space.tex the Fix can't be processed.
---
 library/numbers.tex                         | 19 ++++++++
 library/topology/metric-space.tex           |  2 +-
 library/topology/real-topological-space.tex | 73 +++++++++++++++++++++++++++--
 library/topology/urysohn2.tex               | 73 ++++++++++++++++++++++++-----
 4 files changed, 149 insertions(+), 18 deletions(-)

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

diff --git a/library/numbers.tex b/library/numbers.tex
index cb3d5cf..b7de307 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -245,12 +245,31 @@
     Then $(n + m) + (k + l)= n + m + k + l = n + (m + k) + l = (((n + m) + k) + l)$.    
 \end{proposition}
 
+%\begin{proposition}\label{natural_disstro_oneline}
+%    Suppose $n,m,k \in \naturals$.
+%    Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$.
+%\end{proposition}
+%\begin{proof}
+%    Let $P = \{n \in \naturals \mid \forall m,k \in \naturals .  n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$.
+%    $\zero \in P$.
+%    $P \subseteq \naturals$.
+%    It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
+%    Fix $n \in P$.
+%    It suffices to show that for all $m'$ such that $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n} \rmul (m' + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$.
+%    Fix $m' \in \naturals$.
+%    Fix $k' \in \naturals$.
+%    $n \in \naturals$.
+%    $ \suc{n} \rmul (m' + k') = (n \rmul (m' + k')) + (m' + k') = ((n \rmul m') + (n \rmul k')) + (m' + k')  = ((n \rmul m') + (n \rmul k')) + m' + k'    = (((n \rmul m') + (n \rmul k')) + m') + k'  = (m' + ((n \rmul m') + (n \rmul k'))) + k'  = ((m' + (n \rmul m')) + (n \rmul k')) + k'  = (((n \rmul m') + m') + (n \rmul k')) + k'  = ((n \rmul m') + m') + ((n \rmul k') + k')  = (\suc{n} \rmul m') + (\suc{n} \rmul k')$.
+%\end{proof}
+
 \begin{proposition}\label{natural_disstro}
     Suppose $n,m,k \in \naturals$.
     Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$.
 \end{proposition}
 \begin{proof}
+   %Let $P = \{n \in \naturals \mid \forall m,k \in \naturals . n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$.
     Let $P = \{n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$}\}$.
+
     $\zero \in P$.
     $P \subseteq \naturals$.
     It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index bcc5b8c..0ed7bab 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -7,7 +7,7 @@
 \section{Metric Spaces}
 
 \begin{definition}\label{metric}
-    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and
+    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reaaals$ and
     for all $x,y,z \in M$ we have 
         $f(x,x) = \zero$ and 
         $f(x,y) = f(y,x)$ and
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index 239965c..db46732 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -17,10 +17,73 @@
     $\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.
+\begin{axiom}\label{reals_carrier_reals}
+    $\carrier[\reals] = \reals$.
+\end{axiom}
+
+\begin{theorem}\label{topological_basis_reals_is_prebasis}
+    $\topoBasisReals$ is a topological prebasis for $\reals$.
 \end{theorem}
 \begin{proof}
-    Omitted.
-\end{proof}
\ No newline at end of file
+    We show that $\unions{\topoBasisReals} \subseteq \reals$.
+    \begin{subproof}
+        It suffices to show that for all $x \in \unions{\topoBasisReals}$ we have $x \in \reals$.
+        Fix $x \in \unions{\topoBasisReals}$.
+    \end{subproof}
+    We show that $\reals \subseteq \unions{\topoBasisReals}$.
+    \begin{subproof}
+        It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$.
+        Fix $x \in \reals$.
+    \end{subproof}
+\end{proof}
+
+\begin{theorem}\label{topological_basis_reals_is_basis}
+    $\topoBasisReals$ is a topological basis for $\reals$.
+\end{theorem}
+\begin{proof}
+    $\topoBasisReals$ is a topological prebasis for $\reals$ by \cref{topological_basis_reals_is_prebasis}.
+    Let $B = \topoBasisReals$.
+    It suffices to show that for all $U \in B$ we have for all $V \in B$ we have for all $x$ such that $x \in U, V$ there exists $W\in B$ such that $x\in W\subseteq U, V$.
+    Fix $U \in B$.
+    Fix $V \in B$.
+    Fix $x \in U, V$.
+\end{proof}
+
+\begin{axiom}\label{topological_space_reals}
+    $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$.
+\end{axiom}
+
+\begin{theorem}\label{reals_is_topological_space}
+    $\reals$ is a topological space.
+\end{theorem}
+\begin{proof}
+    $\topoBasisReals$ is a topological basis for $\reals$.
+    Let $B = \topoBasisReals$.
+    We show that $\opens[\reals]$ is a family of subsets of $\carrier[\reals]$.
+    \begin{subproof}
+        It suffices to show that for all $A \in \opens[\reals]$ we have $A \subseteq \reals$.
+        Fix $A \in \opens[\reals]$.
+        Follows by \cref{powerset_elim,topological_space_reals,genopens}.
+    \end{subproof}
+    We show that $\reals \in\opens[\reals]$.
+    \begin{subproof}
+        $B$ covers $\reals$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
+        $\unions{B} \in \genOpens{B}{\reals}$.
+        $\reals \subseteq \unions{B}$.
+    \end{subproof}
+    We show that for all $A, B\in \opens[\reals]$ we have $A\inter B\in\opens[\reals]$.
+    \begin{subproof}
+        Follows by \cref{topological_space_reals,inters_in_genopens}.
+    \end{subproof}
+    We show that for all $F\subseteq \opens[\reals]$ we have $\unions{F}\in\opens[\reals]$.
+    \begin{subproof}
+        Follows by \cref{topological_space_reals,union_in_genopens}.
+    \end{subproof}
+    $\carrier[\reals] = \reals$.
+    Follows by \cref{topological_space}.
+\end{proof}
+
+\begin{proposition}\label{open_interval_is_open}
+    Suppose $a,b \in \reals$.
+    Then $\intervalopen{a}{b} \in \opens[\reals]$.
+\end{proposition}
\ No newline at end of file
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 396255e..838b121 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -152,16 +152,23 @@
 \begin{proposition}\label{no_natural_between_n_and_suc_n}
     For all $n,m \in \naturals$ we have not $n < m < \suc{n}$.
 \end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{naturals_is_zero_one_or_greater}
+    $\naturals = \{n \in \naturals \mid n > 1 \lor n = 1 \lor n = \zero\}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
 
 \begin{proposition}\label{naturals_rless_existence_of_lesser_natural}
     For all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ there exist $k \in \naturals$ such that $m + k = n$.
 \end{proposition}
 \begin{proof}[Proof by \in-induction on $n$]
     Assume $n \in \naturals$.
-    We show that $\naturals = (\{\zero, 1\} \union \{n \in \naturals \mid n > 1\})$.
-    \begin{subproof}
-        Trivial.
-    \end{subproof}
+    
     \begin{byCase}
         \caseOf{$n = \zero$.} 
             
@@ -196,9 +203,17 @@
         We show that for all $m \in \naturals$ such that$m < n$ we have $m \in n$.
         \begin{subproof}[Proof by \in-induction on $m$]
             Assume $m \in \naturals$.
-            %\begin{byCase}
-            %    
-            %\end{byCase}
+            \begin{byCase}
+                \caseOf{$\suc{m}=n$.}
+                \caseOf{$\suc{m}\neq n$.}  
+                      \begin{byCase}
+                        \caseOf{$n = \zero$.}
+                        \caseOf{$n \neq \zero$.}
+                            Take $l \in \naturals$ such that $\suc{l} = n$.
+                            Omitted.
+
+                      \end{byCase}
+            \end{byCase}
         \end{subproof}
     \end{subproof}
     
@@ -323,17 +338,51 @@
     For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
 \end{proposition}
 
+\begin{proposition}\label{bijection_naturals_order}
+    For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
 \begin{proposition}\label{existence_normal_ordered_urysohn}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain of $X$.
     Suppose $\dom{U}$ is finite.
-    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $X$ to $Y$ and $V$ is normal ordered.
+    Suppose $U$ is inhabited.
+    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $U$ to $V$ and $V$ is normal ordered.
 \end{proposition}
 \begin{proof}
-    Take $k$ such that $\dom{U}$ has cardinality $k$ by \cref{ran_converse,cardinality,finite}.
-    There exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$.
-
-
+    Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}.
+    \begin{byCase}
+        \caseOf{$n = \zero$.} 
+            Omitted.
+        \caseOf{$n \neq \zero$.}
+            Take $k$ such that $k \in \naturals$ and $\suc{k}=n$. 
+            We have $\dom{U} \subseteq \naturals$.
+            $\dom{U}$ is inhabited.
+            We show that there exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
+            \begin{subproof}
+                Omitted.
+            \end{subproof}
+            Let $N = \seq{\zero}{k}$.
+            Let $M = \pow{X}$.
+            Define $V : N \to M$ such that $V(n)=$
+            \begin{cases}
+                &\at{U}{F(n)} & \text{if} n \in N
+            \end{cases}
+            $\dom{V} = \seq{\zero}{k}$.
+            We show that $V$ is a urysohnchain of $X$.
+            \begin{subproof}
+                Trivial.
+            \end{subproof}
+            We show that $F$ is consistent on $U$ to $V$.
+            \begin{subproof}
+                Trivial.
+            \end{subproof}
+            $V$ is normal ordered.
+    \end{byCase}
+    
 \end{proof}
 
 
-- 
cgit v1.2.3


From 588c6ab14184cab4bb7df89def641acaafe3b7eb Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 16 Sep 2024 11:34:01 +0200
Subject: working commit

---
 latex/naproche.sty                          |  20 +-
 latex/stdlib.tex                            |   4 +-
 library/topology/real-topological-space.tex | 121 ++++++-
 library/topology/urysohn.tex                | 515 ++++++++++++++--------------
 library/topology/urysohn2.tex               |  14 +-
 5 files changed, 387 insertions(+), 287 deletions(-)

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

diff --git a/latex/naproche.sty b/latex/naproche.sty
index 5ca673d..1a8afb6 100644
--- a/latex/naproche.sty
+++ b/latex/naproche.sty
@@ -40,6 +40,7 @@
 \newtheorem{remark}[theoremcount]{Remark}
 \newtheorem{signature}[theoremcount]{Signature}
 \newtheorem{theorem}[theoremcount]{Theorem}
+\newtheorem{inductive}[theoremcount]{Inductive}
 
 % Theorem environments without numbering.
 \newtheorem*{quotedaxiom}{Axiom}
@@ -139,9 +140,22 @@
 \newcommand{\rationals}{\mathcal{Q}}
 \newcommand{\rminus}{-_{\mathcal{R}}}
 \newcommand{\seq}[2]{\{#1, ... ,#2\}}
-\newcommand{\indexx}[2]{index_{#1}(#2)}
-\newcommand{\indexset}[2]{#1}
-
+\newcommand{\indexx}[2][]{index_{#1}(#2)}
+\newcommand{\indexxset}[1]{#1}
+\newcommand{\topoBasisReals}{\mathbb{B}_{\mathcal{R}}}
+\newcommand{\intervalopen}[2]{(#1, #2)}
+\newcommand{\intervalclosed}[2]{[#1, #2]}
+\newcommand{\epsBall}[2]{\mathcal{B}_{#1,#2}}
+\newcommand{\realsplus}{\reals_{+}}
+\newcommand{\rless}{<}
+\newcommand{\two}{2}
+\newcommand{\powerOfTwoSet}{\mathbb{P}_{2^{}}}
+\newcommand{\pot}{\powerOfTwoSet}
+\newcommand{\chain}[1]{#1}
+\newcommand{\refine}{\text{ finer than }}
+\newcommand{\abs}[1]{\left\lvert#1\right\rvert}
+\newcommand{\realsminus}{\reals_{-}}
+\newcommand{\at}[2]{#1(#2)}
 
 
 \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol
diff --git a/latex/stdlib.tex b/latex/stdlib.tex
index 2faa267..9879708 100644
--- a/latex/stdlib.tex
+++ b/latex/stdlib.tex
@@ -47,5 +47,7 @@
     \input{../library/topology/disconnection.tex}
     \input{../library/numbers.tex}
     \input{../library/topology/urysohn.tex}
-    \input{../library/wunschzettel.tex}
+    \input{../library/topology/urysohn2.tex}
+    \input{../library/topology/real-topological-space.tex}
+    %\input{../library/wunschzettel.tex}
 \end{document}
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index 1c5e4cb..ffdf46e 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -11,7 +11,7 @@
 \import{function.tex}
 
 
-\section{The canonical topology on $\mathbbR$}
+\section{The canonical topology on $\mathbb{R}$}
 
 \begin{definition}\label{topological_basis_reals_eps_ball}
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
@@ -101,12 +101,15 @@
     For all $x,y \in \reals$ such that $x < y$ we have there exists $z \in \realsplus$ such that $x + z = y$.
 \end{lemma}
 \begin{proof}
-    %Fix $x,y \in \reals$.
+    Omitted.
 \end{proof}
 
 \begin{lemma}\label{reals_order_is_transitive}
     For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$.
 \end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
 
 \begin{lemma}\label{reals_order_plus_minus}
     Suppose $a,b \in \reals$.
@@ -134,16 +137,9 @@
     $x + \epsilon \in \reals$.
 
 
-    %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)$.
+    $(x - \epsilon) < c < (x + \epsilon)$.
 \end{proof}
 
 \begin{theorem}\label{topological_basis_reals_is_prebasis}
@@ -158,9 +154,9 @@
             \caseOf{$x = \emptyset$.}
                 Trivial.
             \caseOf{$x \neq \emptyset$.}
-                There exists $U \in \topoBasisReals$ such that $x \in \topoBasisReals$.
-                Take $U \in \topoBasisReals$ such that $x \in \topoBasisReals$.
-
+                %There exists $U \in \topoBasisReals$ such that $x \in U$.
+                Take $U \in \topoBasisReals$ such that $x \in U$.
+                Follows by \cref{epsball_are_subseteq_reals_set,topological_basis_reals_eps_ball,epsilon_ball,minus,subseteq}.
         \end{byCase}
     \end{subproof}
     We show that $\reals \subseteq \unions{\topoBasisReals}$.
@@ -168,10 +164,63 @@
         It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$.
         Fix $x \in \reals$.
         $\epsBall{x}{1} \in \topoBasisReals$.
-        Therefore $x \in \unions{\topoBasisReals}$.
+        Therefore $x \in \unions{\topoBasisReals}$ by \cref{one_in_reals,reals_one_bigger_zero,unions_intro,realsplus,plus_one_order,reals_order_minus_positiv,epsball_are_connected_in_reals}.
     \end{subproof}
 \end{proof}
 
+%\begin{lemma}\label{intervl_intersection_is_interval}
+%    Suppose $a,b,a',b' \in \reals$.
+%    Suppose there exist $x \in \reals$ such that $x \in \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$.
+%    Then there exists $q,p \in \reals$ such that $q < p$ and $\intervalopen{q}{p} \subseteq \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$.
+%\end{lemma}
+%
+
+\begin{lemma}\label{reals_order_total}
+    For all $x,y \in \reals$ we have either $x < y$ or $x \geq y$. 
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $x \in \reals$ we have for all $y \in \reals$ we have either $x < y$ or $x \geq y$. 
+    Fix $x \in \reals$.
+    Fix $y \in \reals$.
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{topo_basis_reals_eps_iff}
+    $X \in \topoBasisReals$ iff there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} = X$.
+\end{lemma}
+
+\begin{lemma}\label{topo_basis_reals_intro}
+For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have $\epsBall{x}{\delta} \in \topoBasisReals$.
+\end{lemma}
+
+\begin{lemma}\label{realspuls_in_reals_plus}
+    For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x + y \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{realspuls_in_reals_minus}
+    For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x - y \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{eps_ball_implies_open_interval}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$. 
+    Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
+\end{lemma}
+
+\begin{lemma}\label{open_interval_eq_eps_ball}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then there exist $x,\epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
+\end{lemma}
+\begin{proof}
+    Let $\delta = (b-a)$.
+    $\delta$ is positiv by \cref{minus_}.
+    There exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$.
+
+\end{proof}
+
+
+
 \begin{theorem}\label{topological_basis_reals_is_basis}
     $\topoBasisReals$ is a topological basis for $\reals$.
 \end{theorem}
@@ -188,7 +237,45 @@
             Trivial.
         \caseOf{$U \inter V \neq \emptyset$.}
             Then $U \inter V$ is inhabited.
-            %It suffices to show that 
+            $x \in \reals$ by \cref{inter_lower_left,subseteq,topological_prebasis_iff_covering_family,omega_is_an_ordinal,naturals_subseteq_reals,subset_transitive,suc_subseteq_elim,ordinal_suc_subseteq}.
+            There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$.
+            There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$.
+            Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$.
+            Then $ (x_2 - \beta) < x < (x_2 + \beta)$.
+            We show that if there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$ then there exists $W\in B$ such that $x\in W\subseteq U, V$.
+            \begin{subproof}
+                Suppose there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$.
+                $x \in \epsBall{x}{\delta}$.
+                $\epsBall{x}{\delta} \subseteq U$.
+                $\epsBall{x}{\delta} \subseteq V$.
+                $\epsBall{x}{\delta} \in B$.
+            \end{subproof}
+            It suffices to show that there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$.
+
+
+            %It suffices to show that there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} \subseteq u \inter V$.
+            %There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$.
+            %There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$.
+            %Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$.
+            %Then $ (x_2 - \beta) < x < (x_2 + \beta)$.
+            %\begin{byCase}
+            %    \caseOf{$x_1 = x_2$.}
+            %        Take $\gamma \in \realsplus$ such that either $\gamma = \alpha \land \gamma \leq \beta$ or $\gamma \leq \alpha \land \gamma = \beta$.
+            %    \caseOf{$x_1 < x_2$.}
+            %    \caseOf{$x_1 > x_2$.}
+            %\end{byCase}
+            %%Take $m$ such that $m \in \min{\{(x_1 + \alpha), (x_2 + \beta)\}}$.
+            %Take $n$ such that $n \in \max{\{(x_1 - \alpha), (x_2 - \beta)\}}$.
+            %Then $m < x < n$.
+            %We show that there exists $x_1 \in \reals$ such that $x_1 \in U \inter V$ and $x_1 < x$.
+            %\begin{subproof}
+            %    Suppose not.
+            %    Then For all $y \in U \inter V$ we have $x \leq y$.
+            %\end{subproof}
+            %We show that there exists $x_2 \in \reals$ such that $x_2 \in U \inter V$ and $x_2 > x$.
+            %\begin{subproof}
+            %    Trivial.
+            %\end{subproof}
     \end{byCase}
 \end{proof}
 
@@ -230,7 +317,3 @@
     Suppose $a,b \in \reals$.
     Then $\intervalopen{a}{b} \in \opens[\reals]$.
 \end{proposition}
-
-\begin{lemma}\label{safetwo}
-    Contradiction.
-\end{lemma}
\ No newline at end of file
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 17e2911..ff6a231 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -51,13 +51,14 @@ The first tept will be a formalisation of chain constructions.
 \begin{struct}\label{sequence}
     A sequence $X$ is a onesorted structure equipped with
     \begin{enumerate}
-        \item $\index$
-        \item $\indexset$
+        \item $\indexx$
+        \item $\indexxset$
+        
     \end{enumerate}
     such that
     \begin{enumerate}
-        \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$.
-        \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$.
+        \item\label{indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$.
+        \item\label{index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$.
     \end{enumerate}
 \end{struct}
 
@@ -68,13 +69,13 @@ The first tept will be a formalisation of chain constructions.
 
 \begin{definition}\label{cahin_of_subsets}
     $C$ is a chain of subsets iff
-    $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$.
+    $C$ is a sequence and for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\indexx[C](n) \subseteq \indexx[C](m)$.
 \end{definition}
 
 \begin{definition}\label{chain_of_n_subsets}
     $C$ is a chain of $n$ subsets iff
-    $C$ is a chain of subsets and $n \in \indexset[C]$ 
-    and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexset[C]$.
+    $C$ is a chain of subsets and $n \in \indexxset[C]$ 
+    and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexxset[C]$.
 \end{definition}
 
 
@@ -133,18 +134,18 @@ The first tept will be a formalisation of chain constructions.
         \item \label{staircase_domain} $\dom{f}$ is a topological space.
         \item \label{staricase_def_chain} $C$ is a chain of subsets.
         \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
-        \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. 
+        \item \label{staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. 
         \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
-        \item \label{staircase_chain_indeset} There exist $n$ such that $\indexset[C] = \seq{\zero}{n}$.
-        \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexset[C]$ 
-            such that $n \neq \zero$ we have $f(\index[C](n) \setminus \index[C](n-1)) = \rfrac{n}{ \max{\indexset[C]} }$. 
+        \item \label{staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$.
+        \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ 
+            such that $n \neq \zero$ we have $f(\indexx[C](n) \setminus \indexx[C](n-1)) = \rfrac{n}{ \max{\indexxset[C]} }$. 
     \end{enumerate}
 \end{struct}
 
 \begin{definition}\label{legal_staircase}
     $f$ is a legal staircase function iff
     $f$ is a staircase function and 
-    for all $n,m \in \indexset[\chain[f]]$ such that $n \leq m$ we have $f(\index[\chain[f]](n)) \leq f(\index[\chain[f]](m))$.
+    for all $n,m \in \indexxset[\chain[f]]$ such that $n \leq m$ we have $f(\indexx[\chain[f]](n)) \leq f(\indexx[\chain[f]](m))$.
 \end{definition}
 
 \begin{abbreviation}\label{urysohnspace}
@@ -159,23 +160,23 @@ The first tept will be a formalisation of chain constructions.
     $C$ is a urysohnchain in $X$ of cardinality $k$ iff %<---- TODO: cardinality unused!
     $C$ is a chain of subsets and
     for all $A \in C$ we have $A \subseteq X$ and
-    for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$.
+    for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$.
 \end{definition}
 
 \begin{definition}\label{urysohnchain_without_cardinality}
     $C$ is a urysohnchain in $X$ iff
     $C$ is a chain of subsets and
     for all $A \in C$ we have $A \subseteq X$ and
-    for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$.
+    for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$.
 \end{definition}
 
 \begin{abbreviation}\label{infinte_sequence}
-    $S$ is a infinite sequence iff $S$ is a sequence and $\indexset[S]$ is infinite.
+    $S$ is a infinite sequence iff $S$ is a sequence and $\indexxset[S]$ is infinite.
 \end{abbreviation}
 
 \begin{definition}\label{infinite_product}
     $X$ is the infinite product of $Y$ iff
-    $X$ is a infinite sequence and for all $i \in \indexset[X]$ we have $\index[X](i) = Y$.
+    $X$ is a infinite sequence and for all $i \in \indexxset[X]$ we have $\indexx[X](i) = Y$.
 \end{definition}
 
 \begin{definition}\label{refinmant}
@@ -289,9 +290,9 @@ The first tept will be a formalisation of chain constructions.
     Suppose $A \inter B$ is empty.
     Then there exist $U$
     such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
-    and $\indexset[U]= \{\zero, 1\}$
-    and $\index[U](\zero) = A$
-    and $\index[U](1) = (\carrier[X] \setminus B)$.
+    and $\indexxset[U]= \{\zero, 1\}$
+    and $\indexx[U](\zero) = A$
+    and $\indexx[U](1) = (\carrier[X] \setminus B)$.
     %$U$ is a urysohnchain in $X$.
 \end{proposition}
 \begin{proof}
@@ -310,12 +311,12 @@ The first tept will be a formalisation of chain constructions.
 %   
     %   We show that $U$ is a chain of subsets.
     %   \begin{subproof}
-    %       For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$.
-    %       It suffices to show that for all $n \in \indexset[U]$ we have
-    %       for all $m \in \indexset[U]$ such that 
-    %       $n < m$ we have $\index[U](n) \subseteq \index[U](m)$.
-    %       Fix $n \in \indexset[U]$.
-    %       Fix $m \in \indexset[U]$.
+    %       For all $n \in \indexxset[U]$ we have $n = \zero \lor n = 1$.
+    %       It suffices to show that for all $n \in \indexxset[U]$ we have
+    %       for all $m \in \indexxset[U]$ such that 
+    %       $n < m$ we have $\indexx[U](n) \subseteq \indexx[U](m)$.
+    %       Fix $n \in \indexxset[U]$.
+    %       Fix $m \in \indexxset[U]$.
     %       \begin{byCase}
     %           \caseOf{$n = 1$.} Trivial.
     %           \caseOf{$n = \zero$.} 
@@ -337,8 +338,8 @@ The first tept will be a formalisation of chain constructions.
     %   \begin{subproof}
     %       Omitted.
     %   \end{subproof}
-    %   We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have
-    %   $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$.
+    %   We show that for all $n,m \in \indexxset[U]$ such that $n < m$ we have
+    %   $\closure{\indexx[U](n)}{X} \subseteq \interior{\indexx[U](m)}{X}$.
     %   \begin{subproof}
     %       Omitted.
     %   \end{subproof}
@@ -352,9 +353,9 @@ The first tept will be a formalisation of chain constructions.
     Suppose $A \inter B$ is empty.
     Suppose there exist $U$
     such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
-    and $\indexset[U]= \{\zero, 1\}$
-    and $\index[U](\zero) = A$
-    and $\index[U](1) = (\carrier[X] \setminus B)$.
+    and $\indexxset[U]= \{\zero, 1\}$
+    and $\indexx[U](\zero) = A$
+    and $\indexx[U](1) = (\carrier[X] \setminus B)$.
     Then $U$ is a urysohnchain in $X$.
 \end{proposition}
 \begin{proof}
@@ -384,9 +385,9 @@ The first tept will be a formalisation of chain constructions.
     % U  = ( A_{0}, A_{1}, A_{2}, ... , A_{n-1}, A_{n})
     % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ...   A_{n-1}, A'_{n}, A_{n})
 
-    % Let $m = \max{\indexset[U]}$.
-    % For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
-    % such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$.
+    % Let $m = \max{\indexxset[U]}$.
+    % For all $n \in (\indexxset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
+    % such that $\closure{\indexx[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\indexx[U](n+1)}{X}$.
     
     
     %\begin{definition}\label{refinmant}
@@ -408,7 +409,7 @@ The first tept will be a formalisation of chain constructions.
     Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$.
     Suppose $k \neq \zero$.
     Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
-    and for all $n \in \indexset[U]$ we have for all $x \in \index[U](n)$ 
+    and for all $n \in \indexxset[U]$ we have for all $x \in \indexx[U](n)$ 
     we have $f(x) = \rfrac{n}{k}$.
 \end{proposition}
 \begin{proof}
@@ -445,11 +446,11 @@ The first tept will be a formalisation of chain constructions.
 
 \begin{abbreviation}\label{converge}
     $s$ converges iff $s$ is a sequence of real numbers 
-    and $\indexset[s]$ is infinite
+    and $\indexxset[s]$ is infinite
     and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have
-    there exist $N \in \indexset[s]$ such that
-    for all $m \in \indexset[s]$ such that $m > N$ 
-    we have $\abs{\index[s](N) - \index[s](m)} < \epsilon$.
+    there exist $N \in \indexxset[s]$ such that
+    for all $m \in \indexxset[s]$ such that $m > N$ 
+    we have $\abs{\indexx[s](N) - \indexx[s](m)} < \epsilon$.
 \end{abbreviation}
 
 
@@ -457,9 +458,9 @@ The first tept will be a formalisation of chain constructions.
     $x$ is the limit of $s$ iff $s$ is a sequence of real numbers
     and $x \in \reals$ and 
     for all $\epsilon \in \reals$ such that $\epsilon > \zero$
-    we have there exist $n \in \indexset[s]$ such that 
-    for all $m \in \indexset[s]$ such that $m > n$ 
-    we have $\abs{x - \index[s](n)} < \epsilon$.
+    we have there exist $n \in \indexxset[s]$ such that 
+    for all $m \in \indexxset[s]$ such that $m > n$ 
+    we have $\abs{x - \indexx[s](n)} < \epsilon$.
 \end{definition}
 
 \begin{proposition}\label{existence_of_limit}
@@ -473,9 +474,9 @@ The first tept will be a formalisation of chain constructions.
 
 \begin{definition}\label{limit_sequence}
     $x$ is the limit sequence of $f$ iff
-    $x$ is a sequence and $\indexset[x] = \dom{f}$ and
-    for all $n \in \indexset[x]$ we have
-    $\index[x](n) = f(n)$.
+    $x$ is a sequence and $\indexxset[x] = \dom{f}$ and
+    for all $n \in \indexxset[x]$ we have
+    $\indexx[x](n) = f(n)$.
 \end{definition}
 
 \begin{definition}\label{realsminus}
@@ -596,15 +597,15 @@ The first tept will be a formalisation of chain constructions.
 \begin{proof}
     
     There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ 
-    and $\indexset[\eta] = \{\zero, 1\}$ 
-    and $\index[\eta](\zero) = A$
-    and $\index[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnchain_induction_begin}.
+    and $\indexxset[\eta] = \{\zero, 1\}$ 
+    and $\indexx[\eta](\zero) = A$
+    and $\indexx[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnchain_induction_begin}.
     
     We show that there exist $\zeta$ such that $\zeta$ is a sequence 
-    and $\indexset[\zeta] = \naturals$
-    and $\eta \in \carrier[\zeta]$ and $\index[\zeta](\eta) = \zero$
-    and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ 
-    and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$.
+    and $\indexxset[\zeta] = \naturals$
+    and $\eta \in \carrier[\zeta]$ and $\indexx[\zeta](\eta) = \zero$
+    and for all $n \in \indexxset[\zeta]$ we have $n+1 \in \indexxset[\zeta]$ 
+    and $\indexx[\zeta](n+1)$ is a refinmant of $\indexx[\zeta](n)$.
     \begin{subproof}
             %Let $\alpha = \{x \in C \mid \exists y \in \alpha. x \refine y \lor x = \eta\}$.
             %Let $\beta = \{ (n,x) \mid n \in \naturals \mid \exists m \in \naturals. \exists y \in \alpha. (x \in \alpha) \land ((x \refine y \land m = n+1 )\lor ((n,x) = (\zero,\eta)))\}$.
@@ -614,7 +615,7 @@ The first tept will be a formalisation of chain constructions.
             %$\dom{\beta} = \naturals$.
             %$\ran{\beta} = \alpha$.
             %$\beta \in \funs{\naturals}{\alpha}$.
-            %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexset[\zeta] = \naturals$ and $\index[\zeta] = \beta$.
+            %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexxset[\zeta] = \naturals$ and $\indexx[\zeta] = \beta$.
         Omitted.
     \end{subproof}
 
@@ -628,14 +629,14 @@ The first tept will be a formalisation of chain constructions.
     %We show that there exist $k \in \funs{\carrier[X]}{\reals}$ such that
     %$k(x)$
 
-    %For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$.
+    %For all $n \in \naturals$ we have $\indexx[\zeta](n)$ is a urysohnchain in $X$.
 
-    We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$.
+    We show that for all $n \in \indexxset[\zeta]$ we have $\indexx[\zeta](n)$ has cardinality $\pot(n)$.
     \begin{subproof}
         Omitted.
     \end{subproof}
 
-    We show that for all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$.
+    We show that for all $m \in \indexxset[\zeta]$ we have $\pot(m) \neq \zero$.
     \begin{subproof}
         Omitted.
     \end{subproof}
@@ -646,212 +647,212 @@ The first tept will be a formalisation of chain constructions.
     \end{subproof}
 
     
-    We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
-    and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ such that $x \notin \index[\index[\zeta](m)](n-1)$ 
-    we have $f(x) = \rfrac{n}{\pot(m)}$.
-    \begin{subproof}
-        Fix $m \in \indexset[\zeta]$.
-        %$\index[\zeta](m)$ is a urysohnchain in $X$.
-
-        %Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$
-        %\begin{cases}
-        %    & 0  & \text{if} x \in A 
-        %    & 1 & \text{if} x \in B 
-        %    & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1)
-        %\end{cases}
+%    We show that for all $m \in \indexxset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
+%    and for all $n \in \indexxset[\indexx[\zeta](m)]$ we have for all $x \in \indexx[\indexx[\zeta](m)](n)$ such that $x \notin \indexx[\indexx[\zeta](m)](n-1)$ 
+%    we have $f(x) = \rfrac{n}{\pot(m)}$.
+%    \begin{subproof}
+%        Fix $m \in \indexxset[\zeta]$.
+%        %$\indexx[\zeta](m)$ is a urysohnchain in $X$.
 %
-        Omitted.
-    \end{subproof}
-
-    
-
-    %The sequenc of the functions
-    Let $\gamma = \{
-        (n,f) \mid 
-        n \in \naturals \mid 
-        
-        \forall n' \in \indexset[\index[\zeta](n)].             
-        \forall x \in \carrier[X].      
-        
-
-        f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land
-
-
-        % (n,f) \in \gamma  <=>   \phi(n,f)
-        % with \phi (n,f) :=        
-        %    (x \in (A_k) \ (A_k-1)) ==> f(x) = ( k / 2^n )        
-        % \/ (x \notin A_k for all k \in {1,..,n} ==>  f(x) = 1 
-
-            (       (n' = \zero)   
-            \land   (x \in \index[\index[\zeta](n)](n')) 
-            \land   (f(x)= \zero) ) 
-        
-        \lor
-        
-            (       (n' > \zero)    
-            \land   (x \in \index[\index[\zeta](n)](n'))
-            \land   (x \notin \index[\index[\zeta](n)](n'-1))
-            \land   (f(x) = \rfrac{n'}{\pot(n)}) )
-            
-        \lor
-
-            (       (x \notin  \index[\index[\zeta](n)](n'))
-            \land   (f(x) = 1) )
-        
-    \}$.
-    
-    Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$.
-
-    We show that for all $n \in \naturals$ we have $\gamma(n)$ 
-    is a function from $\carrier[X]$ to $\reals$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    
-    We show that for all $n \in \naturals$ we have $\gamma(n)$ 
-    is a function from $\carrier[X]$ to $\intervalclosed{\zero}{1}$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    We show that $\gamma$ is a function from $\naturals$ to $\reals$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    We show that  for all $x,k,n$ such that $n\in \naturals$ and $k \in \naturals$ and $x \in \index[\index[\zeta](n)](k)$ we have $\apply{\gamma(n)}{x} =  \rfrac{k}{\pot(n)}$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. 
-    \begin{subproof}
-        Fix $n \in \naturals$.
-        Fix $x \in \carrier[X]$.
-        Omitted.
-    \end{subproof}
-
-
-
-    We show that 
-    if $h$ is a function from $\naturals$ to $\reals$ and for all $n \in \naturals$ we have $h(n) \leq h(n+1)$ and there exist $B \in \reals$ such that $h(n) < B$ 
-    then there exist $k \in \reals$ such that for all $m \in \naturals$ we have $h(m) \leq k$ and for all $k' \in \reals$ such that $k' < k$ we have there exist $M \in \naturals$ such that $k' < h(M)$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof} 
-
-
-
-    We show that there exist $g$ such that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that  $g(x)= k$ and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
-    \begin{subproof}       
-        We show that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
-        \begin{subproof}
-            Fix $x \in \carrier[X]$.
-            
-            Omitted.
-            
-            % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
-            %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
-        \end{subproof}
-        Omitted.
-    \end{subproof}
-    
-
-    Let $G(x) = g(x)$ for $x \in \carrier[X]$.
-    We have $\dom{G} = \carrier[X]$.
-
-    We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$.
-    \begin{subproof}
-        %Fix $x \in \dom{G}$.
-        %It suffices to show that $g(x) \in \reals$.
+%        %Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$
+%        %\begin{cases}
+%        %    & 0  & \text{if} x \in A 
+%        %    & 1 & \text{if} x \in B 
+%        %    & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \indexx[\indexx[\zeta](m)](n) \land x \notin \indexx[\indexx[\zeta](m)](n-1)
+%        %\end{cases}
+%%
+%        Omitted.
+%    \end{subproof}
 %
-        %There exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
+%    
 %
-        %We show that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - g(x)} < \epsilon$ and $g(x)= k$.
-        %\begin{subproof}
-        %    Fix $\epsilon \in \reals$.
-        %    
+%    %The sequenc of the functions
+%    Let $\gamma = \{
+%        (n,f) \mid 
+%        n \in \naturals \mid 
+%        
+%        \forall n' \in \indexxset[\indexx[\zeta](n)].             
+%        \forall x \in \carrier[X].      
+%        
 %
-        %\end{subproof}
-        %Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
-        Omitted.
-    \end{subproof}
-
-    We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$.
-    \begin{subproof}
-        %Fix $x \in \dom{G}$.
-        %Then $x \in \carrier[X]$.
-        %\begin{byCase}
-        %    \caseOf{$x \in A$.} 
-        %        For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$.
-%
-%
-        %    \caseOf{$x \notin A$.} 
-        %        \begin{byCase}
-        %            \caseOf{$x \in B$.} 
-        %                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
-%
-        %            \caseOf{$x \notin B$.}
-        %                Omitted.
-        %        \end{byCase}
-        %\end{byCase}
-        Omitted.
-    \end{subproof}
-
-
-    We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
-    \begin{subproof}        
-        %It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}.
-        %It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$.
-        %Fix $x \in \dom{G}$.
-        %Then $x \in \carrier[X]$.
-        %$g(x) = G(x)$.
-        %We have $G(x) \in \reals$.
-        %$\zero \leq G(x) \leq 1$.
-        %We have $G(x) \in \intervalclosed{\zero}{1}$ .
-        Omitted.
-    \end{subproof}
-
-    We show that $G(A) = \zero$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    We show that $G(B) = 1$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    We show that $G$ is continuous.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    %Suppose $\eta$ is a urysohnchain in $X$.
-    %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
-    %and $\indexset[\eta] = \{\zero, 1\}$
-    %and $\index[\eta](\zero) = A$ 
-    %and $\index[\eta](1) = (X \setminus B)$.
-
-
-    %Then $\eta$ is a urysohnchain in $X$.
-
-    %   Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$.
-    %   
-    %   We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence 
-    %   and for all $i \in \indexset[\zeta]$ we have 
-    %   $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$
-    %   and $A \subseteq \index[\zeta](i)$
-    %   and $\index[\zeta](i) \subseteq (X \setminus B)$
-    %   and for all $j \in \indexset[\zeta]$ such that 
-    %   $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$.
-    %   \begin{subproof}
-    %       Omitted.
-    %   \end{subproof}
-    %   
-    %   
-    %   
+%        f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land
+%
+%
+%        % (n,f) \in \gamma  <=>   \phi(n,f)
+%        % with \phi (n,f) :=        
+%        %    (x \in (A_k) \ (A_k-1)) ==> f(x) = ( k / 2^n )        
+%        % \/ (x \notin A_k for all k \in {1,..,n} ==>  f(x) = 1 
+%
+%            (       (n' = \zero)   
+%            \land   (x \in \indexx[\indexx[\zeta](n)](n')) 
+%            \land   (f(x)= \zero) ) 
+%        
+%        \lor
+%        
+%            (       (n' > \zero)    
+%            \land   (x \in \indexx[\indexx[\zeta](n)](n'))
+%            \land   (x \notin \indexx[\indexx[\zeta](n)](n'-1))
+%            \land   (f(x) = \rfrac{n'}{\pot(n)}) )
+%            
+%        \lor
+%
+%            (       (x \notin  \indexx[\indexx[\zeta](n)](n'))
+%            \land   (f(x) = 1) )
+%        
+%    \}$.
+%    
+%    Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$.
+%
+%    We show that for all $n \in \naturals$ we have $\gamma(n)$ 
+%    is a function from $\carrier[X]$ to $\reals$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    
+%    We show that for all $n \in \naturals$ we have $\gamma(n)$ 
+%    is a function from $\carrier[X]$ to $\intervalclosed{\zero}{1}$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $\gamma$ is a function from $\naturals$ to $\reals$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that  for all $x,k,n$ such that $n\in \naturals$ and $k \in \naturals$ and $x \in \indexx[\indexx[\zeta](n)](k)$ we have $\apply{\gamma(n)}{x} =  \rfrac{k}{\pot(n)}$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. 
+%    \begin{subproof}
+%        Fix $n \in \naturals$.
+%        Fix $x \in \carrier[X]$.
+%        Omitted.
+%    \end{subproof}
+%
+%
+%
+%    We show that 
+%    if $h$ is a function from $\naturals$ to $\reals$ and for all $n \in \naturals$ we have $h(n) \leq h(n+1)$ and there exist $B \in \reals$ such that $h(n) < B$ 
+%    then there exist $k \in \reals$ such that for all $m \in \naturals$ we have $h(m) \leq k$ and for all $k' \in \reals$ such that $k' < k$ we have there exist $M \in \naturals$ such that $k' < h(M)$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof} 
+%
+%
+%
+%    We show that there exist $g$ such that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that  $g(x)= k$ and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
+%    \begin{subproof}       
+%        We show that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
+%        \begin{subproof}
+%            Fix $x \in \carrier[X]$.
+%            
+%            Omitted.
+%            
+%            % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
+%            %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
+%        \end{subproof}
+%        Omitted.
+%    \end{subproof}
+%    
+%
+%    Let $G(x) = g(x)$ for $x \in \carrier[X]$.
+%    We have $\dom{G} = \carrier[X]$.
+%
+%    We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$.
+%    \begin{subproof}
+%        %Fix $x \in \dom{G}$.
+%        %It suffices to show that $g(x) \in \reals$.
+%%
+%        %There exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
+%%
+%        %We show that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - g(x)} < \epsilon$ and $g(x)= k$.
+%        %\begin{subproof}
+%        %    Fix $\epsilon \in \reals$.
+%        %    
+%%
+%        %\end{subproof}
+%        %Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$.
+%    \begin{subproof}
+%        %Fix $x \in \dom{G}$.
+%        %Then $x \in \carrier[X]$.
+%        %\begin{byCase}
+%        %    \caseOf{$x \in A$.} 
+%        %        For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$.
+%%
+%%
+%        %    \caseOf{$x \notin A$.} 
+%        %        \begin{byCase}
+%        %            \caseOf{$x \in B$.} 
+%        %                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
+%%
+%        %            \caseOf{$x \notin B$.}
+%        %                Omitted.
+%        %        \end{byCase}
+%        %\end{byCase}
+%        Omitted.
+%    \end{subproof}
+%
+%
+%    We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
+%    \begin{subproof}        
+%        %It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}.
+%        %It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$.
+%        %Fix $x \in \dom{G}$.
+%        %Then $x \in \carrier[X]$.
+%        %$g(x) = G(x)$.
+%        %We have $G(x) \in \reals$.
+%        %$\zero \leq G(x) \leq 1$.
+%        %We have $G(x) \in \intervalclosed{\zero}{1}$ .
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $G(A) = \zero$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $G(B) = 1$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $G$ is continuous.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    %Suppose $\eta$ is a urysohnchain in $X$.
+%    %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
+%    %and $\indexxset[\eta] = \{\zero, 1\}$
+%    %and $\indexx[\eta](\zero) = A$ 
+%    %and $\indexx[\eta](1) = (X \setminus B)$.
+%
+%
+%    %Then $\eta$ is a urysohnchain in $X$.
+%
+%    %   Take $P$ such that $P$ is a infinite sequence and $\indexxset[P] = \naturals$ and for all $i \in \indexxset[P]$ we have $\indexx[P](i) = \pow{X}$.
+%    %   
+%    %   We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence 
+%    %   and for all $i \in \indexxset[\zeta]$ we have 
+%    %   $\indexx[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$
+%    %   and $A \subseteq \indexx[\zeta](i)$
+%    %   and $\indexx[\zeta](i) \subseteq (X \setminus B)$
+%    %   and for all $j \in \indexxset[\zeta]$ such that 
+%    %   $j < i$ we have for all $x \in \indexx[\zeta](j)$ we have $x \in \indexx[\zeta](i)$.
+%    %   \begin{subproof}
+%    %       Omitted.
+%    %   \end{subproof}
+%    %   
+%    %   
+%    %   
     %   
     %   
     %   
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 838b121..83e3aa4 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -367,10 +367,10 @@
             \end{subproof}
             Let $N = \seq{\zero}{k}$.
             Let $M = \pow{X}$.
-            Define $V : N \to M$ such that $V(n)=$
+            Define $V : N \to M$ such that $V(n)=
             \begin{cases}
-                &\at{U}{F(n)} & \text{if} n \in N
-            \end{cases}
+                \at{U}{F(n)} & \text{if} n \in N
+            \end{cases}$
             $\dom{V} = \seq{\zero}{k}$.
             We show that $V$ is a urysohnchain of $X$.
             \begin{subproof}
@@ -445,11 +445,11 @@
     $B \subseteq X'$ by \cref{powerset_elim,closeds}.
     $A \subseteq X'$.
     Therefore $A \subseteq A'$.
-    Define $U_0: N \to \{A, A'\}$ such that $U_0(n) =$
+    Define $U_0: N \to \{A, A'\}$ such that $U_0(n) =
     \begin{cases}
-        &A  &\text{if} n = \zero \\
-        &A' &\text{if} n = 1
-    \end{cases}
+        A  &\text{if} n = \zero \\
+        A' &\text{if} n = 1
+    \end{cases}$
     $U_0$ is a function.
     $\dom{U_0} = N$.
     $\dom{U_0} \subseteq \naturals$ by \cref{ran_converse}. 
-- 
cgit v1.2.3


From a9785eb4cac6b8c237173f7e14367babd79e92e1 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 17 Sep 2024 03:39:23 +0200
Subject: working commit

---
 library/topology/real-topological-space.tex | 36 +++++++++------
 library/topology/urysohn2.tex               | 72 ++++++++++++++++++++++++++---
 2 files changed, 86 insertions(+), 22 deletions(-)

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

diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index d9790aa..b2e5ea9 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -382,7 +382,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
             We have $a',b' \in \reals$ by assumption.
             We have $a' < b'$ by \cref{id_img,epsilon_ball,minus,intervalopen,reals_order_is_transitive}.
             Then there exist $x',\epsilon'$ such that $x' \in \reals$ and $\epsilon' \in \realsplus$ and $\intervalopen{a'}{b'} = \epsBall{x'}{\epsilon'}$.
-            Then $x \in \epsBall{x'}{\epsilon'}$.
+            Then $x \in \epsBall{x'}{\epsilon'}$ by \cref{epsilon_ball}.
 
             Follows by \cref{inter_lower_left,inter_lower_right,epsilon_ball,topological_basis_reals_eps_ball}.
             %Then $(x_1 - \alpha) < (x_2 + \beta)$.
@@ -536,7 +536,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
         \begin{subproof}
             It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteLeft{a}$.
             Fix $x \in \unions{E}$.
-            Take $e \in E$ such that $x \in e$.
+            Take $e \in E$ such that $x \in e$ by \cref{unions_iff}.
             $x \in \reals$.
             Take $x',\delta'$ such that $x' \in \reals$ and $\delta' \in \realsplus$ and $e = \epsBall{x'}{\delta'}$ by \cref{epsilon_ball,minus,topo_basis_reals_eps_iff,setminus,setminus_emptyset,elem_subseteq}.
             $\epsBall{x'}{\delta'} \in E$.
@@ -550,8 +550,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
                 Suppose not.
                 Take $y' \in e$ such that $y' > a$. 
                 $x'' < a$.
-                $(x'' - \delta'') < y' < (x'' + \delta'')$.
-                $(x'' - \delta'') < x'' < (x'' + \delta'')$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$ by \cref{minus,intervalopen,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$ by \cref{minus,intervalopen,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
                 Then $x'' < a < y'$.
                 Therefore $(x'' - \delta'') < a < (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_left,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq}.
                 Then $a \in e$ by \cref{epsball_are_connected_in_reals,intervalopen_infinite_left,neq_witness}.
@@ -565,7 +565,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
             Trivial.
         \end{subproof}
     \end{subproof}
-    $\unions{E} \in \opens[\reals]$.
+    $\unions{E} \in \opens[\reals]$ by \cref{opens_unions,reals_is_topological_space,basis_is_in_genopens,topological_space_reals,topological_basis_reals_is_basis,subset_transitive}.
 \end{proof}
 
 \begin{lemma}\label{continuous_on_basis_implies_continuous_endo}
@@ -600,7 +600,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
         \begin{subproof}
             It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteRight{a}$.
             Fix $x \in \unions{E}$.
-            Take $e \in E$ such that $x \in e$.
+            Take $e \in E$ such that $x \in e$ by \cref{unions_iff}.
             $x \in \reals$.
             Take $x',\delta'$ such that $x' \in \reals$ and $\delta' \in \realsplus$ and $e = \epsBall{x'}{\delta'}$ by \cref{epsilon_ball,minus,topo_basis_reals_eps_iff,setminus,setminus_emptyset,elem_subseteq}.
             $\epsBall{x'}{\delta'} \in E$.
@@ -612,10 +612,10 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
                 There exists $x'' \in \intervalopenInfiniteRight{a}$ such that there exists $\delta'' \in \realsplus$ such that $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
                 Take $x'',\delta''$ such that $x'' \in \intervalopenInfiniteRight{a}$ and $\delta'' \in \realsplus$ and $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
                 Suppose not.
-                Take $y' \in e$ such that $y' < a$. 
+                Take $y' \in e$ such that $y' < a$ by \cref{reals_order_total,intervalopen,eps_ball_implies_open_interval}. 
                 $x'' > a$.
-                $(x'' - \delta'') < y' < (x'' + \delta'')$.
-                $(x'' - \delta'') < x'' < (x'' + \delta'')$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$ by \cref{minus,intervalopen,intervalclosed,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$ by \cref{minus,intervalopen,intervalclosed,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
                 Then $x'' > a > y'$.
                 Therefore $(x'' - \delta'') > a > (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_right,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq,epsball_are_connected_in_reals,subseteq}.
                 Then $a \in e$ by \cref{reals_order_is_transitive,reals_order_total,reals_add,realsplus,epsball_are_connected_in_reals,intervalopen_infinite_right,neq_witness}.
@@ -689,6 +689,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     We show that for all $x \in \reals$ we have $x \in (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b})$.
     \begin{subproof}
         Fix $x \in \reals$.
+        Follows by \cref{union_intro_left,intervalopen_infinite_left,reals_order_total,reals_order_total2,union_iff,intervalopen_infinite_right,union_assoc,union_intro_right,intervalclosed}.
     \end{subproof}
 \end{proof}
 
@@ -697,7 +698,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalclosedInfiniteRight{a}$.
 \end{lemma}
 \begin{proof}
-    It suffices to show that for all $x \in \reals$ we have either $x \in \intervalopenInfiniteLeft{a}$ or $x \in \intervalclosedInfiniteRight{a}$.
+    It suffices to show that for all $x \in \reals$ we have either $x \in \intervalopenInfiniteLeft{a}$ or $x \in \intervalclosedInfiniteRight{a}$ by \cref{intervalopen_infinite_left,union_intro_left,neq_witness,intervalclosed_infinite_right,union_intro_right,union_iff}.
     Trivial.
 \end{proof}
 
@@ -714,6 +715,9 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Suppose $a \in \reals$.
     Then $\intervalopenInfiniteRight{a} \inter \intervalclosedInfiniteLeft{a} = \emptyset$.
 \end{lemma}
+\begin{proof}
+    Follows by \cref{reals_order_total,inter_lower_left,intervalopen_infinite_right,order_reals_lemma6,inter_lower_right,foundation,subseteq,intervalclosed_infinite_left}.
+\end{proof}
 
 \begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_left}
     Suppose $a \in \reals$.
@@ -725,7 +729,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
     Then $\intervalclosedInfiniteRight{a} \in \closeds{\reals}$.
 \end{proposition}
 \begin{proof}
-    $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$.
+    $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$ by \cref{intersection_of_open_closed__infinite_intervals_open_left,reals_as_union_of_open_closed_intervals2,setminus_inter,double_relative_complement,subseteq_union_setminus,subseteq_setminus,setminus_union,setminus_disjoint,setminus_partition,setminus_subseteq,setminus_emptyset,setminus_self,setminus_setminus,double_complement_union}.
 \end{proof}
 
 \begin{proposition}\label{closedinterval_infinite_left_in_closeds}
@@ -747,15 +751,17 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have
         We show that for all $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$ we have $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
         \begin{subproof}
             Fix $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$.
-            Then $x \in \reals \setminus \intervalopenInfiniteLeft{a}$.
-            Then $x \in \reals \setminus \intervalopenInfiniteRight{b}$.
+            Then $x \in \reals \setminus \intervalopenInfiniteLeft{a}$ by \cref{setminus,double_complement_union}.
+            Then $x \in \reals \setminus \intervalopenInfiniteRight{b}$ by \cref{union_upper_left,subseteq,union_comm,subseteq_implies_setminus_supseteq}.
+            Follows by \cref{inter_intro}.
         \end{subproof}
         We show that for all $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$ we have $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$.
         \begin{subproof}
             Fix $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
-            Then $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$.
-            Then $x \in (\reals \setminus \intervalopenInfiniteRight{b})$.
+            Then $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$ by \cref{setminus_setminus,setminus}.
+            Then $x \in (\reals \setminus \intervalopenInfiniteRight{b})$ by \cref{inter_lower_right,elem_subseteq,setminus_setminus}.
         \end{subproof}
+        Follows by \cref{setminus_union}.
     \end{subproof}
     We show that $\reals \setminus \intervalopenInfiniteLeft{a} = \intervalclosedInfiniteRight{a}$.
     \begin{subproof}
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 83e3aa4..9990199 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -94,6 +94,9 @@
 \begin{proposition}\label{naturals_in_transitive}
     $\naturals$ is a \in-transitive set.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{nat_is_transitiveset}.
+\end{proof}
 
 \begin{proposition}\label{naturals_elem_in_transitive}
     If $n \in \naturals$ then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
@@ -119,6 +122,9 @@
 \begin{proposition}\label{zero_is_empty}
     There exists no $x$ such that $x \in \zero$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{notin_emptyset}.
+\end{proof}
 
 \begin{proposition}\label{one_is_positiv}
     $1$ is positiv.
@@ -163,6 +169,13 @@
     Omitted.
 \end{proof}
 
+\begin{proposition}\label{naturals_one_zero_or_greater}
+    For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{reals_order,naturals_subseteq_reals,subseteq,one_in_reals,naturals_is_zero_one_or_greater}.
+\end{proof}
+
 \begin{proposition}\label{naturals_rless_existence_of_lesser_natural}
     For all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ there exist $k \in \naturals$ such that $m + k = n$.
 \end{proposition}
@@ -184,7 +197,7 @@
             \end{subproof}
         \caseOf{$n = 1$.}
             Fix $m$.
-            For all $l \in \naturals$ we have If $l < 1$ then $l = \zero$.
+            For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$.
             Then $\zero + 1 = 1$.
         \caseOf{$n > 1$.} 
             Take $l \in \naturals$ such that $\suc{l} = n$.
@@ -350,7 +363,7 @@
     Suppose $U$ is a urysohnchain of $X$.
     Suppose $\dom{U}$ is finite.
     Suppose $U$ is inhabited.
-    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $U$ to $V$ and $V$ is normal ordered.
+    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $V$ to $U$ and $V$ is normal ordered.
 \end{proposition}
 \begin{proof}
     Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}.
@@ -360,11 +373,36 @@
         \caseOf{$n \neq \zero$.}
             Take $k$ such that $k \in \naturals$ and $\suc{k}=n$. 
             We have $\dom{U} \subseteq \naturals$.
-            $\dom{U}$ is inhabited.
+            $\dom{U}$ is inhabited by \cref{downward_closure,downward_closure_iff,rightunique,function_member_elim,inhabited,chain_of_subsets,urysohnchain,sequence}.
+            $\dom{U}$ has cardinality $\suc{k}$.
             We show that there exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
             \begin{subproof}
-                Omitted.
+                For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$.
+                We have $\dom{U} \subseteq \naturals$.
+                $\dom{U}$ is inhabited.
+                Therefore there exist $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}.
+                We show that $\seq{\zero}{k'} = \seq{\zero}{k}$.
+                \begin{subproof}
+                    We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$.
+                    \begin{subproof}
+                        It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$.
+                        Fix $y \in \seq{\emptyset}{k'}$.
+                        Then $y \leq k'$.
+                        Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}.
+                        %Then $\seq{\emptyset}{k'} \in \suc{k}$.
+                        Therefore $y \in \suc{k}$.
+                        Therefore $y \in \seq{\emptyset}{k}$.
+                    \end{subproof}
+                    We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$.
+                    \begin{subproof}
+                        Fix $y \in \seq{\emptyset}{k}$.
+                    \end{subproof}
+                \end{subproof}
             \end{subproof}
+            Take $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
             Let $N = \seq{\zero}{k}$.
             Let $M = \pow{X}$.
             Define $V : N \to M$ such that $V(n)=
@@ -374,11 +412,31 @@
             $\dom{V} = \seq{\zero}{k}$.
             We show that $V$ is a urysohnchain of $X$.
             \begin{subproof}
-                Trivial.
+                It suffices to show that $V$ is a chain of subsets in $X$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$.
+                We show that $V$ is a chain of subsets in $X$.
+                \begin{subproof}
+                    It suffices to show that $V$ is a sequence and for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    $V$ is a sequence by \cref{m_to_n_set,sequence,subseteq}.
+                    It suffices to show that for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    Fix $n \in \dom{V}$.
+                    Then $\at{V}{n} \subseteq \carrier[X]$ by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+                    It suffices to show that for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    Fix $m$ such that $m \in \dom{V}$ and $n \rless m$.
+                    Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+                \end{subproof}
+                It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V} \land n \rless m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$.
+                Fix $n \in \dom{V}$.
+                Fix $m$ such that $m \in \dom{V} \land n \rless m$.
+                Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
             \end{subproof}
-            We show that $F$ is consistent on $U$ to $V$.
+            We show that $F$ is consistent on $V$ to $U$.
             \begin{subproof}
-                Trivial.
+                It suffices to show that $F$ is a bijection from $\dom{V}$ to $\dom{U}$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $F(n) < F(m)$ by \cref{bijection_of_urysohnchains}.
+                $F$ is a bijection from $\dom{V}$ to $\dom{U}$.
+                It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $f(n) < f(m)$.
+                Fix $n \in \dom{V}$.
+                Fix $m$ such that $m \in \dom{V}$ and $n \rless m$.
+                Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
             \end{subproof}
             $V$ is normal ordered.
     \end{byCase}
-- 
cgit v1.2.3


From c943ca6441e9118bc9caee1c11f697da89bc06b7 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 18 Sep 2024 00:01:42 +0200
Subject: working commit

---
 library/set/equinumerosity.tex |   2 +-
 library/topology/urysohn2.tex  | 260 ++++++++++++++++++++++++++++++++++++++---
 source/Checking.hs             |   2 +-
 source/Meaning.hs              |   4 +-
 source/Syntax/Abstract.hs      |   2 +-
 source/Syntax/Concrete.hs      |   4 +-
 source/Syntax/Internal.hs      |   2 +-
 7 files changed, 250 insertions(+), 26 deletions(-)

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

diff --git a/library/set/equinumerosity.tex b/library/set/equinumerosity.tex
index a846b78..a922052 100644
--- a/library/set/equinumerosity.tex
+++ b/library/set/equinumerosity.tex
@@ -15,7 +15,7 @@
     $A\approx A$.
 \end{proposition}
 \begin{proof}
-    $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_is_bijection}.
+    $\identity{A}$ is a bijection from $A$ to $A$. %by \cref{id_is_bijection}.
     Follows by \cref{equinum}.
 \end{proof}
 
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 9990199..97bbc70 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -13,6 +13,7 @@
 \import{set/fixpoint.tex}
 \import{set/product.tex}
 \import{topology/real-topological-space.tex}
+\import{set/equinumerosity.tex}
 
 \section{Urysohns Lemma}
 
@@ -251,6 +252,7 @@
 
 
 
+
 \begin{proposition}\label{naturals_leq_on_suc}
     For all $n,m \in \naturals$ such that $m < \suc{n}$ we have $m \leq n$.
 \end{proposition}
@@ -358,6 +360,218 @@
     Omitted.
 \end{proof}
 
+\begin{lemma}\label{naturals_suc_injective}
+    Suppose $n,m \in \naturals$.
+    $n = m$ iff $\suc{n} = \suc{m}$.
+\end{lemma}
+
+\begin{lemma}\label{naturals_rless_implies_not_eq}
+    Suppose $n,m \in \naturals$.
+    Suppose $n < m$.
+    Then $n \neq m$.
+\end{lemma}
+
+\begin{lemma}\label{cardinality_of_singleton}
+    For all $x$ such that $x \neq \emptyset$ we have $\{x\}$ has cardinality $1$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+    %Fix $x$.
+    %Suppose $x \neq \emptyset$.
+    %Let $X = \{x\}$.
+    %$\seq{\zero}{\zero}=1$.
+    %$\seq{\zero}{\zero}$ has cardinality $1$.
+    %$X \setminus \{x\} = \emptyset$.
+    %$1 = \{\emptyset\}$.
+    %Let $F = \{(x,\emptyset)\}$.
+    %$F$ is a relation.
+    %$\dom{F} = X$.
+    %$\emptyset \in \ran{F}$.
+    %for all $x \in 1$ we have $x = \emptyset$.
+    %$\ran{F} = 1$.
+    %$F$ is injective.
+    %$F \in \surj{X}{1}$.
+    %$F$ is a bijection from $X$ to $1$.
+\end{proof}
+
+\begin{lemma}\label{cardinality_n_plus_1}
+    For all $n \in \naturals$ we have $n+1$ has cardinality $n+1$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{cardinality_n_m_plus}
+    For all $n,m \in \naturals$ we have $n+m$ has cardinality $n+m$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{cardinality_plus_disjoint}
+    Suppose $X \inter Y = \emptyset$.
+    Suppose $X$ is finite.
+    Suppose $Y$ is finite.
+    Suppose $X$ has cardinality $n$.
+    Suppose $Y$ has cardinality $m$.
+    Then $X \union Y$ has cardinality $m+n$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+
+\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1}
+    Suppose $f$ is a bijection from $X$ to $Y$.
+    Suppose $g$ is a function from $X$ to $Y$.
+    Suppose $g$ is injective.
+    Suppose $X$ is finite and $Y$ is finite. 
+    For all $n \in \naturals$ such that $Y$ has cardinality $n$ we have $g$ is a bijection from $X$ to $Y$.
+\end{lemma}
+\begin{proof}[Proof by \in-induction on $n$]
+    Assume $n \in \naturals$.
+    Suppose $Y$ has cardinality $n$.
+    $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,notin_emptyset}.
+    \begin{byCase}
+        \caseOf{$n = \zero$.} 
+            Follows by \cref{converse_converse_eq,injective_converse_is_function,converse_is_relation,dom_converse,id_is_function_to,id_ran,ran_circ_exact,circ,ran_converse,emptyset_is_function_on_emptyset,bijective_converse_are_funs,relext,function_member_elim,bijection_is_function,cardinality,bijections_dom,in_irrefl,codom_of_emptyset_can_be_anything,converse_emptyset,funs_elim,neq_witness,id}.
+        \caseOf{$n \neq \zero$.}
+            %Take $n' \in n$ such that $n = \suc{n'}$.
+            %$n' \in \naturals$.
+            %$n' + 1 = n$.
+            %Take $y$ such that $y \in Y$ by \cref{funs_type_apply,apply,bijections_to_funs,cardinality,foundation}. 
+            %Let $Y' = Y \setminus \{y\}$.
+            %$Y' \subseteq Y$.
+            %$Y'$ is finite.
+            %There exist $m \in \naturals$ such that $Y'$ has cardinality $m$.
+            %Take $m \in \naturals$ such that $Y'$ has cardinality $m$.
+            %Then $Y'$ has cardinality $n'$.
+            %Let $x' = \apply{\converse{f}}{y'}$. 
+            %$x' \in X$.
+            %Let $X' = X \setminus \{x'\}$.
+            %$X' \subseteq X$.
+            %$X'$ is finite.
+            %There exist $m' \in \naturals$ such that $X'$ has cardinality $m'$.
+            %Take $m' \in \naturals$ such that $X''$ has cardinality $m'$.
+            %Then $X'$ has cardinality $n'$.
+            %Let $f'(z)=f(z)$ for $z \in X'$.
+            %$\dom{f'} = X'$.
+            %$\ran{f'} = Y'$.
+            %$f'$ is a bijection from $X'$ to $Y'$.
+            %Let $g'(z) = g(z)$ for $z \in X'$.
+            %Then $g'$ is injective.
+            %Then $g'$ is a bijection from $X'$ to $Y'$ by \cref{rels,id_elem_rels,times_empty_right,powerset_emptyset,double_complement_union,unions_cons,union_eq_cons,union_as_unions,unions_pow,cons_absorb,setminus_self,bijections_dom,ran_converse,id_apply,apply,unions_emptyset,img_emptyset,zero_is_empty}.
+            %Define $G : X \to Y$ such that $G(z)=
+            %\begin{cases}
+            %    g'(z) & \text{if} z \in X' \\
+            %    y' & \text{if} z = x'
+            %\end{cases}$
+            %$G = g$.
+            %Follows by \cref{double_relative_complement,fun_to_surj,bijections,funs_surj_iff,bijections_to_funs,neq_witness,surj,funs_elim,setminus_self,cons_subseteq_iff,cardinality,ordinal_empty_or_emptyset_elem,naturals_inductive_set,natural_number_is_ordinal_for_all,foundation,inter_eq_left_implies_subseteq,inter_emptyset,cons_subseteq_intro,emptyset_subseteq}.
+            Omitted.
+    \end{byCase}
+    %$\converse{f}$ is a bijection from $Y$ to $X$.
+    %Let $h = g \circ \converse{f}$.
+    %It suffices to show that $\ran{g} = Y$ by \cref{fun_to_surj,dom_converse,bijections}.
+    %It suffices to show that for all $y \in Y$ we have there exist $x \in X$ such that $g(x)=y$ by \cref{funs_ran,subseteq_antisymmetric,fun_ran_iff,apply,funs_elim,ran_converse,subseteq}.
+%
+    %Fix $y \in Y$.
+    %Take $x \in X$ such that $\apply{\converse{f}}{y} = x$.
+
+\end{proof}
+
+\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection}
+    Suppose $f$ is a bijection from $X$ to $Y$.
+    Suppose $g$ is a function from $X$ to $Y$.
+    Suppose $g$ is injective.
+    Suppose $Y$ is finite. 
+    Then $g$ is a bijection from $X$ to $Y$.
+\end{lemma}
+\begin{proof}
+    There exist $n \in \naturals$ such that $Y$ has cardinality $n$ by \cref{cardinality,injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,finite}.
+    Follows by \cref{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,cardinality,equinum_tran,equinum_sym,equinum,finite}.
+\end{proof}
+
+
+
+\begin{lemma}\label{naturals_bijection_implies_eq}
+    Suppose $n,m \in \naturals$.
+    Suppose $f$ is a bijection from $n$ to $m$.
+    Then $n = m$.
+\end{lemma}
+\begin{proof}
+    $n$ is finite.
+    $m$ is finite.
+    Suppose not.
+    Then $n < m$ or $m < n$.
+    \begin{byCase}
+        \caseOf{$n < m$.}
+            Then $n \in m$.
+            There exist $x \in m$ such that $x \notin n$.
+            $\identity{n}$ is a function from $n$ to $m$.
+            $\identity{n}$ is injective.
+            $\apply{\identity{n}}{n} = n$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}.
+            Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}.
+        \caseOf{$m < n$.}
+            Then $m \in n$.
+            There exist $x \in n$ such that $x \notin m$.
+            $\converse{f}$ is a bijection from $m$ to $n$.
+            $\identity{m}$ is a function from $m$ to $n$.
+            $\identity{m}$ is injective.
+            $\apply{\identity{m}}{m} = m$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}.
+            Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}.
+    \end{byCase}
+\end{proof}
+
+\begin{lemma}\label{naturals_eq_iff_bijection}
+    Suppose $n,m \in \naturals$.
+    $n = m$ iff there exist $f$ such that $f$ is a bijection from $n$ to $m$.
+\end{lemma}
+\begin{proof}
+    We show that if $n = m$ then there exist $f$ such that $f$ is a bijection from $n$ to $m$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+    We show that for all $k \in \naturals$ we have if there exist $f$ such that $f$ is a bijection from $k$ to $m$ then $k = m$.
+    \begin{subproof}%[Proof by \in-induction on $k$]
+        %Assume $k \in \naturals$.
+        %\begin{byCase}
+        %    \caseOf{$k = \zero$.} 
+        %        Trivial.
+        %    \caseOf{$k \neq \zero$.}
+        %        \begin{byCase}
+        %            \caseOf{$m = \zero$.}
+        %                Trivial.
+        %            \caseOf{$m \neq \zero$.}
+        %                Take $k' \in \naturals$ such that $\suc{k'} = k$.
+        %                Then $k' \in k$.
+        %                Take $m' \in \naturals$ such that $m = \suc{m'}$.
+        %                Then $m' \in m$.
+        %                
+        %        \end{byCase}
+        %\end{byCase}
+    \end{subproof}
+\end{proof}
+
+\begin{lemma}\label{seq_from_zero_suc_cardinality_eq_upper_border}
+    Suppose $n,m \in \naturals$.
+    Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$.
+    Then $n = m$.
+\end{lemma}
+\begin{proof}
+    We have $\seq{\zero}{n} = \suc{n}$.
+    Take $f$ such that $f$ is a bijection from $\seq{\zero}{n}$ to $\suc{m}$.
+    Therefore $n=m$ by \cref{suc_injective,naturals_inductive_set,cardinality,naturals_eq_iff_bijection}.
+\end{proof}
+
+\begin{lemma}\label{seq_from_zero_cardinality_eq_upper_border_set_eq}
+    Suppose $n,m \in \naturals$.
+    Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$.
+    Then $\seq{\zero}{n} = \seq{\zero}{m}$.
+\end{lemma}
+
 \begin{proposition}\label{existence_normal_ordered_urysohn}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain of $X$.
@@ -384,23 +598,24 @@
                 Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
                 Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
                 $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}.
-                We show that $\seq{\zero}{k'} = \seq{\zero}{k}$.
-                \begin{subproof}
-                    We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$.
-                    \begin{subproof}
-                        It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$.
-                        Fix $y \in \seq{\emptyset}{k'}$.
-                        Then $y \leq k'$.
-                        Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}.
-                        %Then $\seq{\emptyset}{k'} \in \suc{k}$.
-                        Therefore $y \in \suc{k}$.
-                        Therefore $y \in \seq{\emptyset}{k}$.
-                    \end{subproof}
-                    We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$.
-                    \begin{subproof}
-                        Fix $y \in \seq{\emptyset}{k}$.
-                    \end{subproof}
-                \end{subproof}
+                $\seq{\zero}{k'} = \seq{\zero}{k}$ by \cref{omega_is_an_ordinal,seq_from_zero_cardinality_eq_upper_border_set_eq,suc_subseteq_implies_in,suc_subseteq_elim,ordinal_suc_subseteq,cardinality}.
+                %We show that $\seq{\zero}{k'} = \seq{\zero}{k}$.
+                %\begin{subproof}
+                %    We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$.
+                %    \begin{subproof}
+                %        It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$.
+                %        Fix $y \in \seq{\emptyset}{k'}$.
+                %        Then $y \leq k'$.
+                %        Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}.
+                %        
+                %        Therefore $y \in \suc{k}$.
+                %        Therefore $y \in \seq{\emptyset}{k}$.
+                %    \end{subproof}
+                %    We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$.
+                %    \begin{subproof}
+                %        Fix $y \in \seq{\emptyset}{k}$.
+                %    \end{subproof}
+                %\end{subproof}
             \end{subproof}
             Take $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
             Let $N = \seq{\zero}{k}$.
@@ -452,7 +667,9 @@
     $f$ is staircase sequence of $U$ iff $f$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{f}$ and for all $n \in \dom{U}$ we have $\at{f}{n}$ is a staircase function adapted to $\at{U}{n}$ in $U$.
 \end{definition}
 
-
+\begin{definition}
+    
+\end{definition}
 
 
 
@@ -565,8 +782,15 @@
     \end{subproof}
     Take $U$ such that $U$ is a lifted urysohnchain of $X$ and $\at{U}{\zero} = U_0$.
 
+    We show that there exist $S$ such that $S$ is staircase sequence of $U$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    Take $S$ such that $S$ is staircase sequence of $U$.
 
+    For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$.
 
+    We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for .
 
 
     
diff --git a/source/Checking.hs b/source/Checking.hs
index 766c327..8bc38a4 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -543,7 +543,7 @@ checkProof = \case
         checkCalc calc
         assume [Asm (calcResult calc)]
         checkProof continue
-    DefineFunctionMathy funVar argVar domVar ranExpr definitions continue -> do
+    DefineFunctionLocal funVar argVar domVar ranExpr definitions continue -> do
         -- We have f: X \to Y and x \mapsto ...  
         -- definition is a nonempty list of (expresssion e, formula phi)
         -- such that f(x) =  e if phi(x)
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 4a21fa3..00a944f 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -606,9 +606,9 @@ glossProof = \case
             then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
             else error "mismatched variables in function definition."
     
-    Raw.DefineFunctionMathy funVar domVar ranExpr funVar2 argVar definitions proof -> do
+    Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do
         if funVar == funVar2
-            then Sem.DefineFunctionMathy funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
+            then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
             else error "missmatched function names"
     Raw.Calc calc proof ->
         Sem.Calc <$> glossCalc calc <*> glossProof proof
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index 13691e7..c8022c7 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -373,7 +373,7 @@ data Proof
     
     
     
-    | DefineFunctionMathy VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
+    | DefineFunctionLocal VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
     -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
     -- 
     deriving (Show, Eq, Ord)
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 7a89bea..9b947b0 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -374,7 +374,7 @@ grammar lexicon@Lexicon{..} = mdo
     -- \end{cases}
 
     functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula)
-    defineFunctionMathy <-  rule    $ DefineFunctionMathy 
+    defineFunctionLocal <-  rule    $ DefineFunctionLocal 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
                                     <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
                                     <*> (_to *> expr <* endMath <* _suchThat) 
@@ -386,7 +386,7 @@ grammar lexicon@Lexicon{..} = mdo
 
 
 
-    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionMathy, qed]
+    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionLocal, qed]
 
 
     blockAxiom  <- rule $ uncurry3 BlockAxiom     <$> envPos  "axiom" axiom
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index e83126d..c098380 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -446,7 +446,7 @@ data Proof
     | Define VarSymbol Term Proof
     | DefineFunction VarSymbol VarSymbol Term Term Proof
 
-    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
+    | DefineFunctionLocal VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
 
 deriving instance Show Proof
 deriving instance Eq   Proof
-- 
cgit v1.2.3


From 1b05816322dc79b20976350393f71840c697eb46 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 18 Sep 2024 15:09:51 +0200
Subject: Ambiguous parse

in urysohn2.tex line 674 the secound 2 throws an ambiguous parse.
the same definition in line 678 commented without this a does not throe this error.

ambiguous parse: [BlockLemma (SourcePos {sourceName = "set.tex", sourceLine = Pos 129, sourceColumn = Pos 1}) (Marker "empty_eq") (Lemma [] (StmtConnected Implication (StmtVerbPhrase (TermExpr (ExprVar (NamedVar "x")) :| [TermExpr (ExprVar (NamedVar "y"))]) (VPAdj (Adj [Just (Word "empty")] [] :| []))) (StmtFormula (FormulaChain (ChainBase (ExprVar (NamedVar "x") :| []) Positive (RelationSymbol (Symbol "=")) (ExprVar (NamedVar "y") :| [])))))),BlockLemma (SourcePos {sourceName = "set.tex", sourceLine = Pos 129, sourceColumn = Pos 1}) (Marker "empty_eq") (Lemma [] (StmtConnected Implication (StmtConnected Conjunction (StmtVerbPhrase (TermExpr (ExprVar (NamedVar "x")) :| []) (VPVerb (Verb (SgPl {sg = [], pl = []}) []))) (StmtVerbPhrase (TermExpr (ExprVar (NamedVar "y")) :| []) (VPAdj (Adj [Just (Word "empty")] [] :| [])))) (StmtFormula (FormulaChain (ChainBase (ExprVar (NamedVar "x") :| []) Positive (RelationSymbol (Symbol "=")) (ExprVar (NamedVar "y") :| []))))))]
---
 library/topology/urysohn2.tex | 28 +++++++++++++++++++++-------
 1 file changed, 21 insertions(+), 7 deletions(-)

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

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 97bbc70..ce6d742 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -664,14 +664,28 @@
 \end{definition}
 
 \begin{definition}\label{staircase_sequence}
-    $f$ is staircase sequence of $U$ iff $f$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{f}$ and for all $n \in \dom{U}$ we have $\at{f}{n}$ is a staircase function adapted to $\at{U}{n}$ in $U$.
+    $S$ is staircase sequence of $U$ iff $S$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{S}$ and for all $n \in \dom{U}$ we have $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $U$.
 \end{definition}
 
-\begin{definition}
-    
+\begin{definition}\label{staircase_limit_point}
+    $x$ is the staircase limit of $S$ with $y$ iff $x \in \reals$ and for all $\epsilon \in \realsplus$ there exist $n_0 \in \naturals$ such that for all $n \in \naturals$ such that $n_0 \rless n$ we have $\apply{\at{S}{n}}{y} \in \epsBall{x}{\epsilon}$.
 \end{definition}
 
+\begin{definition}\label{staircase_limit_function}
+    $f$ is a limit function of a staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
+\end{definition}
 
+%\begin{definition}\label{staircase_limit_function}
+%    $f$ is a limit function of staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
+%\end{definition}
+%
+%\begin{proposition}\label{staircase_limit_is_continuous}
+%    Suppose $X$ is a urysohnspace.
+%    Suppose $U$ is a lifted urysohnchain of $X$.
+%    Suppose $S$ is staircase sequence of $U$.
+%    Suppose $f$ is the limit function of a staircase $S$.
+%    Then $f$ is continuous.
+%\end{proposition}
 
 \begin{theorem}\label{urysohnsetinbeetween}
     Let $X$ be a urysohn space.
@@ -788,10 +802,10 @@
     \end{subproof}
     Take $S$ such that $S$ is staircase sequence of $U$.
 
-    For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$.
-
-    We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for .
-
+    %For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$.
+%
+    %We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for .
+%
 
     
 \end{proof}
-- 
cgit v1.2.3


From 29f32e2031eafa087323d79d812a1b38ac78f977 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 23 Sep 2024 01:20:05 +0200
Subject: working commit

---
 library/nat.tex                             |  22 +--
 library/topology/real-topological-space.tex |   2 +-
 library/topology/urysohn.tex                | 140 +++++++--------
 library/topology/urysohn2.tex               | 254 +++++++++++++++++++++-------
 4 files changed, 278 insertions(+), 140 deletions(-)

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

diff --git a/library/nat.tex b/library/nat.tex
index ac9a141..841ac36 100644
--- a/library/nat.tex
+++ b/library/nat.tex
@@ -3,48 +3,48 @@
 
 \section{Natural numbers}
 
-\begin{abbreviation}\label{inductive_set}
+\begin{abbreviation}\label{num_inductive_set}
     $A$ is an inductive set iff $\emptyset\in A$ and for all $a\in A$ we have $\suc{a}\in A$.
 \end{abbreviation}
 
-\begin{axiom}\label{naturals_inductive_set}
+\begin{axiom}\label{num_naturals_inductive_set}
     $\naturals$ is an inductive set.
 \end{axiom}
 
-\begin{axiom}\label{naturals_smallest_inductive_set}
+\begin{axiom}\label{num_naturals_smallest_inductive_set}
     Let $A$ be an inductive set.
     Then $\naturals\subseteq A$.
 \end{axiom}
 
-\begin{abbreviation}\label{naturalnumber}
+\begin{abbreviation}\label{num_naturalnumber}
     $n$ is a natural number iff $n\in \naturals$.
 \end{abbreviation}
 
-\begin{lemma}\label{emptyset_in_naturals}
+\begin{lemma}\label{num_emptyset_in_naturals}
     $\emptyset\in\naturals$.    
 \end{lemma}
 
-\begin{signature}\label{addition_is_set}
+\begin{signature}\label{num_addition_is_set}
     $x+y$ is a set.
 \end{signature}
 
-\begin{axiom}\label{addition_on_naturals}
+\begin{axiom}\label{num_addition_on_naturals}
     $x+y$ is a natural number iff $x$ is a natural number and $y$ is a natural number.
 \end{axiom}
 
-\begin{abbreviation}\label{zero_is_emptyset}
+\begin{abbreviation}\label{num_zero_is_emptyset}
     $\zero = \emptyset$.
 \end{abbreviation}
 
-\begin{axiom}\label{addition_axiom_1}
+\begin{axiom}\label{num_addition_axiom_1}
     For all $x \in \naturals$ $x + \zero = \zero + x = x$.
 \end{axiom}
 
-\begin{axiom}\label{addition_axiom_2}
+\begin{axiom}\label{num_addition_axiom_2}
     For all $x, y \in \naturals$ $x + \suc{y} = \suc{x} + y = \suc{x+y}$.
 \end{axiom}
 
-\begin{lemma}\label{naturals_is_equal_to_two_times_naturals}
+\begin{lemma}\label{num_naturals_is_equal_to_two_times_naturals}
     $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
 \end{lemma}
 
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index b2e5ea9..c76fd46 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -11,7 +11,7 @@
 \import{function.tex}
 
 
-\section{The canonical topology on $\mathbb{R}$}
+\section{Topology Reals}
 
 \begin{definition}\label{topological_basis_reals_eps_ball}
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index ff6a231..ae03273 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -36,7 +36,7 @@ The first tept will be a formalisation of chain constructions.
 %           $\overline{A_{i-1}}  \subset \interior{A_{i}}$. 
 %           In this case we call the chain legal.
 
-\begin{definition}\label{one_to_n_set}
+\begin{definition}\label{urysohnone_one_to_n_set}
     $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
 \end{definition}
 
@@ -48,7 +48,7 @@ The first tept will be a formalisation of chain constructions.
 %   together with the existence of an indexing function.
 %
 %%-----------------------
-\begin{struct}\label{sequence}
+\begin{struct}\label{urysohnone_sequence}
     A sequence $X$ is a onesorted structure equipped with
     \begin{enumerate}
         \item $\indexx$
@@ -57,8 +57,8 @@ The first tept will be a formalisation of chain constructions.
     \end{enumerate}
     such that
     \begin{enumerate}
-        \item\label{indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$.
-        \item\label{index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$.
+        \item\label{urysohnone_indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$.
+        \item\label{urysohnone_index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$.
     \end{enumerate}
 \end{struct}
 
@@ -67,12 +67,12 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{definition}\label{cahin_of_subsets}
+\begin{definition}\label{urysohnone_cahin_of_subsets}
     $C$ is a chain of subsets iff
     $C$ is a sequence and for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\indexx[C](n) \subseteq \indexx[C](m)$.
 \end{definition}
 
-\begin{definition}\label{chain_of_n_subsets}
+\begin{definition}\label{urysohnone_chain_of_n_subsets}
     $C$ is a chain of $n$ subsets iff
     $C$ is a chain of subsets and $n \in \indexxset[C]$ 
     and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexxset[C]$.
@@ -84,7 +84,7 @@ The first tept will be a formalisation of chain constructions.
 % and also for the subproof of continuity of the limit.
 
 
-%     \begin{definition}\label{legal_chain}
+%     \begin{definition}\label{urysohnone_legal_chain}
 %         $C$ is a legal chain of subsets of $X$ iff 
 %         $C \subseteq \pow{X}$. %and 
 %         %there exist $f \in \funs{C}{\naturals}$ such that
@@ -106,49 +106,49 @@ The first tept will be a formalisation of chain constructions.
 
 \subsection{staircase function}
 
-\begin{definition}\label{minimum}
+\begin{definition}\label{urysohnone_minimum}
     $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
 \end{definition}
 
-\begin{definition}\label{maximum}
+\begin{definition}\label{urysohnone_maximum}
     $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
 \end{definition}
 
-\begin{definition}\label{intervalclosed}
+\begin{definition}\label{urysohnone_intervalclosed}
     $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
 \end{definition}
 
-\begin{definition}\label{intervalopen}
+\begin{definition}\label{urysohnone_intervalopen}
     $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
 \end{definition}
 
 
-\begin{struct}\label{staircase_function}
+\begin{struct}\label{urysohnone_staircase_function}
     A staircase function $f$ is a onesorted structure equipped with
     \begin{enumerate}
         \item $\chain$
     \end{enumerate}
     such that
     \begin{enumerate}
-        \item \label{staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$.
-        \item \label{staircase_domain} $\dom{f}$ is a topological space.
-        \item \label{staricase_def_chain} $C$ is a chain of subsets.
-        \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
-        \item \label{staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. 
-        \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
-        \item \label{staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$.
-        \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ 
+        \item \label{urysohnone_staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$.
+        \item \label{urysohnone_staircase_domain} $\dom{f}$ is a topological space.
+        \item \label{urysohnone_staricase_def_chain} $C$ is a chain of subsets.
+        \item \label{urysohnone_staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
+        \item \label{urysohnone_staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. 
+        \item \label{urysohnone_staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
+        \item \label{urysohnone_staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$.
+        \item \label{urysohnone_staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ 
             such that $n \neq \zero$ we have $f(\indexx[C](n) \setminus \indexx[C](n-1)) = \rfrac{n}{ \max{\indexxset[C]} }$. 
     \end{enumerate}
 \end{struct}
 
-\begin{definition}\label{legal_staircase}
+\begin{definition}\label{urysohnone_legal_staircase}
     $f$ is a legal staircase function iff
     $f$ is a staircase function and 
     for all $n,m \in \indexxset[\chain[f]]$ such that $n \leq m$ we have $f(\indexx[\chain[f]](n)) \leq f(\indexx[\chain[f]](m))$.
 \end{definition}
 
-\begin{abbreviation}\label{urysohnspace}
+\begin{abbreviation}\label{urysohnone_urysohnspace}
     $X$ is a urysohn space iff
     $X$ is a topological space and
     for all $A,B \in \closeds{X}$ such that $A \inter B = \emptyset$
@@ -156,49 +156,49 @@ The first tept will be a formalisation of chain constructions.
     such that  $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$.    
 \end{abbreviation}
 
-\begin{definition}\label{urysohnchain}
+\begin{definition}\label{urysohnone_urysohnchain}
     $C$ is a urysohnchain in $X$ of cardinality $k$ iff %<---- TODO: cardinality unused!
     $C$ is a chain of subsets and
     for all $A \in C$ we have $A \subseteq X$ and
     for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$.
 \end{definition}
 
-\begin{definition}\label{urysohnchain_without_cardinality}
+\begin{definition}\label{urysohnone_urysohnchain_without_cardinality}
     $C$ is a urysohnchain in $X$ iff
     $C$ is a chain of subsets and
     for all $A \in C$ we have $A \subseteq X$ and
     for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$.
 \end{definition}
 
-\begin{abbreviation}\label{infinte_sequence}
+\begin{abbreviation}\label{urysohnone_infinte_sequence}
     $S$ is a infinite sequence iff $S$ is a sequence and $\indexxset[S]$ is infinite.
 \end{abbreviation}
 
-\begin{definition}\label{infinite_product}
+\begin{definition}\label{urysohnone_infinite_product}
     $X$ is the infinite product of $Y$ iff
     $X$ is a infinite sequence and for all $i \in \indexxset[X]$ we have $\indexx[X](i) = Y$.
 \end{definition}
 
-\begin{definition}\label{refinmant}
+\begin{definition}\label{urysohnone_refinmant}
     $C'$ is a refinmant of $C$ iff $C'$ is a urysohnchain in $X$
     and for all $x \in C$ we have $x \in C'$ 
     and for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$
     and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$.
 \end{definition}
 
-\begin{abbreviation}\label{two}
+\begin{abbreviation}\label{urysohnone_two}
     $\two = \suc{1}$.
 \end{abbreviation}
 
-\begin{lemma}\label{two_in_reals}
+\begin{lemma}\label{urysohnone_two_in_reals}
     $\two \in \reals$.
 \end{lemma}
 
-\begin{lemma}\label{two_in_naturals}
+\begin{lemma}\label{urysohnone_two_in_naturals}
     $\two \in \naturals$.
 \end{lemma}
 
-\begin{inductive}\label{power_of_two}
+\begin{inductive}\label{urysohnone_power_of_two}
     Define $\powerOfTwoSet \subseteq (\naturals \times \naturals)$.
     \begin{enumerate}
         \item  $(\zero, 1) \in \powerOfTwoSet$.
@@ -206,45 +206,45 @@ The first tept will be a formalisation of chain constructions.
     \end{enumerate}
 \end{inductive}
 
-\begin{abbreviation}\label{pot}
+\begin{abbreviation}\label{urysohnone_pot}
     $\pot = \powerOfTwoSet$.
 \end{abbreviation}
 
-\begin{lemma}\label{dom_pot}
+\begin{lemma}\label{urysohnone_dom_pot}
     $\dom{\pot} = \naturals$.
 \end{lemma}
 \begin{proof}
     Omitted.
 \end{proof}
 
-\begin{lemma}\label{ran_pot}
+\begin{lemma}\label{urysohnone_ran_pot}
     $\ran{\pot} \subseteq \naturals$.
 \end{lemma}
 
 
-\begin{axiom}\label{pot1}
+\begin{axiom}\label{urysohnone_pot1}
     $\pot \in \funs{\naturals}{\naturals}$.
 \end{axiom}
 
-\begin{axiom}\label{pot2} 
+\begin{axiom}\label{urysohnone_pot2} 
     For all $n \in \naturals$ we have there exist $k\in \naturals$ such that $(n, k) \in \powerOfTwoSet$ and $\apply{\pot}{n}=k$.
     %$\pot(n) = k$ iff there exist $x \in \powerOfTwoSet$ such that $x = (n,k)$.
 \end{axiom}
 
 
 %Without this abbreviation \pot cant be sed as a function in the standard sense
-\begin{abbreviation}\label{pot_as_function}
+\begin{abbreviation}\label{urysohnone_pot_as_function}
     $\pot(n) = \apply{\pot}{n}$.
 \end{abbreviation}
 
 %Take all points, besids one but then take all open sets not containing x but all other, so \{x\} has to be closed
-\begin{axiom}\label{hausdorff_implies_singltons_closed}
+\begin{axiom}\label{urysohnone_hausdorff_implies_singltons_closed}
     For all $X$ such that $X$ is Hausdorff we have
     for all $x \in \carrier[X]$ we have $\{x\}$ is closed in $X$.
 \end{axiom}
 
 
-\begin{lemma}\label{urysohn_set_in_between}
+\begin{lemma}\label{urysohnone_urysohn_set_in_between}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \subset B$.
@@ -284,7 +284,7 @@ The first tept will be a formalisation of chain constructions.
 \end{proof}
 
 
-\begin{proposition}\label{urysohnchain_induction_begin}
+\begin{proposition}\label{urysohnone_urysohnchain_induction_begin}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
@@ -347,7 +347,7 @@ The first tept will be a formalisation of chain constructions.
     
 \end{proof}
 
-\begin{proposition}\label{urysohnchain_induction_begin_step_two}
+\begin{proposition}\label{urysohnone_urysohnchain_induction_begin_step_two}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
@@ -364,7 +364,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{proposition}\label{t_four_propositon}
+\begin{proposition}\label{urysohnone_t_four_propositon}
     Let $X$ be a urysohn space.
     Then for all $A,B \subseteq X$ such that $\closure{A}{X} \subseteq \interior{B}{X}$
     we have there exists $C \subseteq X$ such that 
@@ -376,7 +376,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{proposition}\label{urysohnchain_induction_step_existence}
+\begin{proposition}\label{urysohnone_urysohnchain_induction_step_existence}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain in $X$.
     Then there exist $U'$ such that $U'$ is a refinmant of $U$ and $U'$ is a urysohnchain in $X$.
@@ -390,7 +390,7 @@ The first tept will be a formalisation of chain constructions.
     % such that $\closure{\indexx[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\indexx[U](n+1)}{X}$.
     
     
-    %\begin{definition}\label{refinmant}
+    %\begin{definition}\label{urysohnone_refinmant}
     %    $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and 
     %    for all $y \in C$ such that $y \subset x$ 
     %    we have there exist $c \in C'$ such that $y \subset c \subset x$
@@ -404,7 +404,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{proposition}\label{existence_of_staircase_function}
+\begin{proposition}\label{urysohnone_existence_of_staircase_function}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$.
     Suppose $k \neq \zero$.
@@ -416,7 +416,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{abbreviation}\label{refinment_abbreviation}
+\begin{abbreviation}\label{urysohnone_refinment_abbreviation}
     $x \refine y$ iff $x$ is a refinmant of $y$.
 \end{abbreviation}
 
@@ -424,27 +424,27 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{abbreviation}\label{sequence_of_functions}
+\begin{abbreviation}\label{urysohnone_sequence_of_functions}
     $f$ is a sequence of functions iff $f$ is a sequence 
     and for all $g \in \carrier[f]$ we have $g$ is a function.
 \end{abbreviation}
 
-\begin{abbreviation}\label{sequence_in_reals}
+\begin{abbreviation}\label{urysohnone_sequence_in_reals}
     $s$ is a sequence of real numbers iff $s$ is a sequence 
     and for all $r \in \carrier[s]$ we have $r \in \reals$.
 \end{abbreviation}
 
 
 
-\begin{axiom}\label{abs_behavior1}
+\begin{axiom}\label{urysohnone_abs_behavior1}
     If $x \geq \zero$ then $\abs{x} = x$.
 \end{axiom}
 
-\begin{axiom}\label{abs_behavior2}
+\begin{axiom}\label{urysohnone_abs_behavior2}
     If $x < \zero$ then $\abs{x} = \neg{x}$.
 \end{axiom}
 
-\begin{abbreviation}\label{converge}
+\begin{abbreviation}\label{urysohnone_converge}
     $s$ converges iff $s$ is a sequence of real numbers 
     and $\indexxset[s]$ is infinite
     and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have
@@ -454,7 +454,7 @@ The first tept will be a formalisation of chain constructions.
 \end{abbreviation}
 
 
-\begin{definition}\label{limit_of_sequence}
+\begin{definition}\label{urysohnone_limit_of_sequence}
     $x$ is the limit of $s$ iff $s$ is a sequence of real numbers
     and $x \in \reals$ and 
     for all $\epsilon \in \reals$ such that $\epsilon > \zero$
@@ -463,7 +463,7 @@ The first tept will be a formalisation of chain constructions.
     we have $\abs{x - \indexx[s](n)} < \epsilon$.
 \end{definition}
 
-\begin{proposition}\label{existence_of_limit}
+\begin{proposition}\label{urysohnone_existence_of_limit}
     Let $s$ be a sequence of real numbers.
     Then $s$ converges iff there exist $x \in \reals$ 
     such that $x$ is the limit of $s$.
@@ -472,22 +472,22 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{definition}\label{limit_sequence}
+\begin{definition}\label{urysohnone_limit_sequence}
     $x$ is the limit sequence of $f$ iff
     $x$ is a sequence and $\indexxset[x] = \dom{f}$ and
     for all $n \in \indexxset[x]$ we have
     $\indexx[x](n) = f(n)$.
 \end{definition}
 
-\begin{definition}\label{realsminus}
+\begin{definition}\label{urysohnone_realsminus}
     $\realsminus = \{r \in \reals \mid r < \zero\}$.
 \end{definition}
 
-\begin{abbreviation}\label{realsplus}
+\begin{abbreviation}\label{urysohnone_realsplus}
     $\realsplus = \reals \setminus \realsminus$.
 \end{abbreviation}
 
-\begin{proposition}\label{intervalclosed_subseteq_reals}
+\begin{proposition}\label{urysohnone_intervalclosed_subseteq_reals}
     Suppose $a,b \in \reals$.
     Suppose $a < b$.
     Then $\intervalclosed{a}{b} \subseteq \reals$.
@@ -495,7 +495,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{lemma}\label{fraction1}
+\begin{lemma}\label{urysohnone_fraction1}
     Let $x \in \reals$.
     Then for all $y \in \reals$ such that $x \neq y$ we have there exists $r \in \rationals$ such that $y < r < x$ or $x < r < y$.
 \end{lemma}
@@ -503,7 +503,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{lemma}\label{frection2}
+\begin{lemma}\label{urysohnone_frection2}
     Suppose $a,b \in \reals$.
     Suppose $a < b$.
     Then $\intervalopen{a}{b}$ is infinite.
@@ -512,7 +512,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{lemma}\label{frection3}
+\begin{lemma}\label{urysohnone_frection3}
     Suppose $a \in \reals$.
     Suppose $a < \zero$.
     Then there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\zero < \rfrac{1}{\pot(N')} < a$. 
@@ -521,7 +521,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{proposition}\label{fraction4}
+\begin{proposition}\label{urysohnone_fraction4}
     Suppose $a,b,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     $\abs{a - b} < \epsilon$ iff $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
@@ -530,7 +530,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{proposition}\label{fraction5}
+\begin{proposition}\label{urysohnone_fraction5}
     Suppose $a,b,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$ iff $a \in \intervalopen{(b - \epsilon)}{(b + \epsilon)}$.
@@ -539,17 +539,17 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{proposition}\label{fraction6}
+\begin{proposition}\label{urysohnone_fraction6}
     Suppose $a,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     $\intervalopen{(a - \epsilon)}{(a + \epsilon)} = \{r \in \reals \mid (a - \epsilon) < r < (a + \epsilon)\} $.
 \end{proposition}
 
-\begin{abbreviation}\label{epsilonball}
+\begin{abbreviation}\label{urysohnone_epsilonball}
     $\epsBall{a}{\epsilon}  = \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
 \end{abbreviation}
 
-\begin{proposition}\label{fraction7}
+\begin{proposition}\label{urysohnone_fraction7}
     Suppose $a,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     Then there exist $b \in \rationals$ such that $b \in \epsBall{a}{\epsilon}$.
@@ -561,11 +561,11 @@ The first tept will be a formalisation of chain constructions.
 
 
  
-%\begin{definition}\label{sequencetwo}
+%\begin{definition}\label{urysohnone_sequencetwo}
 %   $Z$ is a sequencetwo iff  $Z = (N,f,B)$ and $N \subseteq \naturals$ and $f$ is a bijection from $N$ to $B$.
 %\end{definition}
 %
-%\begin{proposition}\label{sequence_existence}
+%\begin{proposition}\label{urysohnone_sequence_existence}
 %    Suppose $N \subseteq \naturals$.
 %    Suppose $M \subseteq \naturals$.
 %    Suppose $N = M$.
@@ -586,7 +586,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{theorem}\label{urysohn}
+\begin{theorem}\label{urysohnone_urysohn1}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
@@ -599,7 +599,7 @@ The first tept will be a formalisation of chain constructions.
     There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ 
     and $\indexxset[\eta] = \{\zero, 1\}$ 
     and $\indexx[\eta](\zero) = A$
-    and $\indexx[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnchain_induction_begin}.
+    and $\indexx[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnone_urysohnchain_induction_begin}.
     
     We show that there exist $\zeta$ such that $\zeta$ is a sequence 
     and $\indexxset[\zeta] = \naturals$
@@ -919,6 +919,6 @@ The first tept will be a formalisation of chain constructions.
     %   \end{subproof}
 \end{proof}
 %
-%\begin{theorem}\label{safe}
+%\begin{theorem}\label{urysohnone_safe}
 %    Contradiction.     
 %\end{theorem}
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index ce6d742..08841da 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -40,7 +40,7 @@
 
 
 \begin{definition}\label{chain_of_subsets}
-    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$ and for all $m \in \dom{X}$ such that $m > n$ we have $\at{X}{n} \subseteq \at{X}{m}$. 
+    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$ and for all $m \in \dom{X}$ such that $n < m$ we have $\at{X}{n} \subseteq \at{X}{m}$. 
 \end{definition}
 
 
@@ -49,11 +49,11 @@
 \end{definition}
 
 \begin{definition}\label{urysohn_finer_set}
-    $A$ is finer between $X$ to $Y$ in $U$ iff $\closure{X}{U} \subseteq \interior{A}{U}$ and $\closure{A}{U} \subseteq \interior{Y}{U}$.
+    $A$ is finer between $B$ to $C$ in $X$ iff $\closure{B}{X} \subseteq \interior{A}{X}$ and $\closure{A}{X} \subseteq \interior{C}{X}$.
 \end{definition}
 
 \begin{definition}\label{finer} %<-- verfeinerung 
-    $Y$ is finer then $X$ in $U$ iff for all $n \in \dom{X}$ we have $\at{X}{n} \in \ran{Y}$ and for all $m \in \dom{X}$ such that $n < m$ we have there exist $k \in \dom{Y}$ such that $\at{Y}{k}$ is finer between $\at{X}{n}$ to $\at{X}{m}$ in $U$.
+    $A$ is finer then $B$ in $X$ iff for all $n \in \dom{B}$ we have $\at{B}{n} \in \ran{A}$ and for all $m \in \dom{B}$ such that $n < m$ we have there exist $k \in \dom{A}$ such that $\at{A}{k}$ is finer between $\at{B}{n}$ to $\at{B}{m}$ in $X$.
 \end{definition}
 
 \begin{definition}\label{follower_index}
@@ -92,6 +92,46 @@
     $f$ is consistent on $X$ to $Y$ iff $f$ is a bijection from $\dom{X}$ to $\dom{Y}$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $f(n) < f(m)$.
 \end{definition}
 
+
+%\begin{definition}\label{staircase}
+%    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and there exist $k \in \naturals$ such that $k = \max{\dom{U}}$ and for all $x,y \in \carrier[X]$ such that $y \in \carrier[X] \setminus \at{U}{k}$ and $x \in \at{U}{k}$ we have $f(y) = 1$ and there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ and $f(x)= \rfrac{m}{k}$.
+%\end{definition}
+
+
+\begin{definition}\label{staircase_step_value1}
+    $a$ is the staircase step value at $y$ of $U$ in $X$ iff there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $y \in \closure{\at{U}{n}}{X} \setminus \closure{\at{U}{m}}{X}$ and $a = \rfrac{n}{\max{\dom{U}}}$.
+\end{definition}
+
+\begin{definition}\label{staircase_step_value2}
+    $a$ is the staircase step valuetwo at $y$ of $U$ in $X$ iff either if $y \in (\carrier[X] \setminus \closure{\at{U}{\max{\dom{U}}}}{X})$ then $a = 1$ or $a$ is the staircase step valuethree at $y$ of $U$ in $X$.
+\end{definition}
+
+\begin{definition}\label{staircase_step_value3}
+    $a$ is the staircase step valuethree at $y$ of $U$ in $X$ iff if $y \in \closure{\at{U}{\min{\dom{U}}}}{X}$ then $f(z) = \zero$.
+\end{definition}
+
+
+\begin{definition}\label{staircase2}
+    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and for all $y \in \carrier[X]$ we have either $f(y)$ is the staircase step value at $y$ of $U$ in $X$ or $f(y)$ is the staircase step valuetwo at $y$ of $U$ in $X$.
+\end{definition}
+
+\begin{definition}\label{staircase_sequence}
+    $S$ is staircase sequence of $U$ in $X$ iff $S$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{S}$ and for all $n \in \dom{U}$ we have $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+\end{definition}
+
+\begin{definition}\label{staircase_limit_point}
+    $x$ is the staircase limit of $S$ with $y$ iff $x \in \reals$ and for all $\epsilon \in \realsplus$ there exist $n_0 \in \naturals$ such that for all $n \in \naturals$ such that $n_0 \rless n$ we have $\apply{\at{S}{n}}{y} \in \epsBall{x}{\epsilon}$.
+\end{definition}
+
+%\begin{definition}\label{staircase_limit_function}
+%    $f$ is a limit function of a staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
+%\end{definition}
+%
+\begin{definition}\label{staircase_limit_function}
+    $f$ is the limit function of staircase $S$ together with $U$ and $X$ iff $S$ is staircase sequence of $U$ in $X$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
+\end{definition}
+
+
 \begin{proposition}\label{naturals_in_transitive}
     $\naturals$ is a \in-transitive set.
 \end{proposition}
@@ -659,33 +699,26 @@
 \end{proof}
 
 
-\begin{definition}\label{staircase}
-    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and for all $x,n,m,k$ such that $k = \max{\dom{U}}$ and $n,m \in \dom{U}$ and $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ we have $f(x)= \rfrac{m}{k}$.
-\end{definition}
-
-\begin{definition}\label{staircase_sequence}
-    $S$ is staircase sequence of $U$ iff $S$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{S}$ and for all $n \in \dom{U}$ we have $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $U$.
-\end{definition}
-
-\begin{definition}\label{staircase_limit_point}
-    $x$ is the staircase limit of $S$ with $y$ iff $x \in \reals$ and for all $\epsilon \in \realsplus$ there exist $n_0 \in \naturals$ such that for all $n \in \naturals$ such that $n_0 \rless n$ we have $\apply{\at{S}{n}}{y} \in \epsBall{x}{\epsilon}$.
-\end{definition}
-
-\begin{definition}\label{staircase_limit_function}
-    $f$ is a limit function of a staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
-\end{definition}
+\begin{proposition}\label{staircase_ran_in_zero_to_one}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain of $X$.
+    Suppose $f$ is a staircase function adapted to $U$ in $X$.
+    Then $\ran{f} \subseteq \intervalclosed{\zero}{1}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
 
-%\begin{definition}\label{staircase_limit_function}
-%    $f$ is a limit function of staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
-%\end{definition}
-%
-%\begin{proposition}\label{staircase_limit_is_continuous}
-%    Suppose $X$ is a urysohnspace.
-%    Suppose $U$ is a lifted urysohnchain of $X$.
-%    Suppose $S$ is staircase sequence of $U$.
-%    Suppose $f$ is the limit function of a staircase $S$.
-%    Then $f$ is continuous.
-%\end{proposition}
+\begin{proposition}\label{staircase_limit_is_continuous}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a lifted urysohnchain of $X$.
+    Suppose $S$ is staircase sequence of $U$ in $X$.
+    Suppose $f$ is the limit function of staircase $S$ together with $U$ and $X$.
+    Then $f$ is continuous.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
 
 \begin{theorem}\label{urysohnsetinbeetween}
     Let $X$ be a urysohn space.
@@ -712,8 +745,26 @@
     Omitted.
 \end{proof}
 
+\begin{lemma}\label{fractions_between_zero_one}
+    Suppose $n,m \in \naturals$.
+    Suppose $m > n$.
+    Then $\zero \leq \rfrac{n}{m} \leq 1$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
 
+\begin{lemma}\label{intervalclosed_border_is_elem}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then $a,b \in \intervalclosed{a}{b}$.  
+\end{lemma}
 
+\begin{lemma}\label{urysohnchain_subseteqrel}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain of $X$.
+    Then for all $n,m \in \dom{U}$ such that $n < m$ we have $\at{U}{n} \subseteq \at{U}{m}$.
+\end{lemma}
 
 
 \begin{theorem}\label{urysohn}
@@ -721,8 +772,8 @@
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
     Suppose $\carrier[X]$ is inhabited.
-    There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
-    and $f(A) = \zero$ and $f(B)= 1$ and $f$ is continuous.
+    There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $f$ is continuous
+    and for all $a,b$ such that $a \in A$ and $b \in B$ we have $f(a)= \zero$ and $f(b) = 1$.
 \end{theorem}
 \begin{proof}
     Let $X' = \carrier[X]$.
@@ -796,46 +847,133 @@
     \end{subproof}
     Take $U$ such that $U$ is a lifted urysohnchain of $X$ and $\at{U}{\zero} = U_0$.
 
-    We show that there exist $S$ such that $S$ is staircase sequence of $U$.
+    We show that there exist $S$ such that $S$ is staircase sequence of $U$ in $X$.
     \begin{subproof}
         Omitted.
     \end{subproof}
-    Take $S$ such that $S$ is staircase sequence of $U$.
+    Take $S$ such that $S$ is staircase sequence of $U$ in $X$.
 
     %For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$.
 %
     %We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for .
-%
+    We show that there exist $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    Take $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$.
+    Then $f$ is continuous.
+    We show that $\dom{f} = \carrier[X]$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+    $f$ is a function.
+    We show that $\ran{f} \subseteq \intervalclosed{\zero}{1}$.
+    \begin{subproof}
+        It suffices to show that $f$ is a function to $\intervalclosed{\zero}{1}$.
+        It suffices to show that for all $x \in \dom{f}$ we have $f(x) \in \intervalclosed{\zero}{1}$.
+        Fix $x \in \dom{f}$.
+        $f(x)$ is the staircase limit of $S$ with $x$.
+        Therefore $f(x) \in \reals$.
+        
+        We show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$.
+        \begin{subproof}
+            Fix $n \in \naturals$.
+            Let $g = \at{S}{n}$.
+            Let $U' = \at{U}{n}$.
+            $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+            $g$ is a staircase function adapted to $U'$ in $X$.
+            $U'$ is a urysohnchain of $X$.
+            $g$ is a function from $\carrier[X]$ to $\reals$.
+            It suffices to show that $\ran{g} \subseteq \intervalclosed{\zero}{1}$ by \cref{function_apply_default,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,function_apply_elim,inter,inter_absorb_supseteq_left,ran_iff,funs_is_relation,funs_is_function,staircase2}.
+            It suffices to show that for all $x \in \dom{g}$ we have $g(x) \in \intervalclosed{\zero}{1}$.
+            Fix $x\in \dom{g}$.
+            Then $x \in \carrier[X]$.
+            \begin{byCase}
+                \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.}
+                    Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$.
+                    Therefore $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    Therefore $x \notin  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.
+                    Then $g(x) = 1$ .
+                \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.}
+                    \begin{byCase}
+                        \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.}
+                            $g(x) = \zero$.
+                        \caseOf{$x \in  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.}
+                            Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$.
+                    \end{byCase}
+            \end{byCase}
+
+            
+
+            %$\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+            %$\at{U}{n}$ is a urysohnchain of $X$.
+            %$\at{S}{n}$ is a function from $\carrier[X]$ to $\reals$.
+            %there exist $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$.
+            %Take $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$.
+            %\begin{byCase}
+            %    \caseOf{$x \in \carrier[X] \setminus \at{\at{U}{n}}{k}$.}
+            %        $1 \in \intervalclosed{\zero}{1}$.
+            %        We show that for all $y \in (\carrier[X] \setminus \at{\at{U}{n}}{k})$ we have $\apply{\at{S}{n}}{y} = 1$.
+            %        \begin{subproof}
+            %            Omitted.
+            %        \end{subproof}
+            %        Then $\apply{\at{S}{n}}{x} = 1$.
+            %    \caseOf{$x \notin \carrier[X] \setminus \at{\at{U}{n}}{k}$.}
+            %        %There exist $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$.
+            %        Take $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$.
+            %        Then  $\apply{\at{S}{n}}{x} = \rfrac{m'}{k'}$.
+            %        It suffices to show that $\rfrac{m'}{k'} \in \intervalclosed{\zero}{1}$.
+            %        $\zero \leq m' \leq k$.
+            %\end{byCase}
+            %%It suffices to show that $\zero \leq \apply{\at{S}{n}}{x} \leq 1$.
+            %%It suffices to show that $\ran{\at{S}{n}} \subseteq \intervalclosed{\zero}{1}$.
+        \end{subproof}
+
+        Suppose not.
+        Then $f(x) < \zero$ or $f(x) > 1$ by \cref{reals_order_total,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,one_in_reals}.
+        For all $\epsilon \in \realsplus$ we have there exist $m \in \naturals$ such that $\apply{\at{S}{m}}{x} \in \epsBall{f(x)}{\epsilon}$ by \cref{plus_one_order,naturals_is_equal_to_two_times_naturals,subseteq,naturals_subseteq_reals,staircase_limit_point}.
+        \begin{byCase}
+            \caseOf{$f(x) < \zero$.}
+                Let $\delta = \zero - f(x)$.
+                $\delta \in \realsplus$.
+                It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$.
+                Fix $n \in \naturals$.
+                $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+                For all $y \in \epsBall{f(x)}{\delta}$ we have $y < \zero$ by \cref{epsilon_ball,minus_behavior1,minus_behavior3,minus,apply,intervalopen}.
+                It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$.
+                Trivial.
+            \caseOf{$f(x) > 1$.}
+                Let $\delta = f(x) - 1$.
+                $\delta \in \realsplus$.
+                It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$.
+                Fix $n \in \naturals$.
+                $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+                For all $y \in \epsBall{f(x)}{\delta}$ we have $y > 1$ by \cref{epsilon_ball,reals_addition_minus_behavior2,minus_in_reals,apply,reals_addition_minus_behavior1,minus,reals_add,realsplus_in_reals,one_in_reals,reals_axiom_kommu,intervalopen}.
+                It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$.
+                Trivial.
+        \end{byCase}
+
+    \end{subproof}
+    Therefore $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ by \cref{staircase_limit_function,surj_to_fun,fun_to_surj,neq_witness,inters_of_ordinals_elem,times_tuple_elim,img_singleton_iff,foundation,subseteq_emptyset_iff,inter_eq_left_implies_subseteq,inter_emptyset,funs_intro,fun_ran_iff,not_in_subseteq}.
+
+    We show that for all $a \in A$ we have $f(a) = \zero$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    We show that for all $b \in B$ we have $f(b) = 1$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
 
-    
 \end{proof}
 
-\begin{theorem}\label{safe}
-    Contradiction.     
-\end{theorem}
+%\begin{theorem}\label{safe}
+%    Contradiction.     
+%\end{theorem}
 
 
 
 
 
-%
-%Ideen:
-%Eine folge ist ein Funktion mit domain \subseteq Natürlichenzahlen. als predicat
-%
-%zulässig und verfeinerung von ketten als predicat definieren. 
-%
-%limits und punkt konvergenz als prädikat.
-%
-%
-%Vor dem Beweis vor dem eigentlichen Beweis.
-%die abgeleiteten Funktionen
-%
-%\derivedstiarcasefunction on A
-%
-%abbreviation: \at{f}{n} = f_{n}
-%
-%
-%TODO:
-%Reals ist ein topologischer Raum
-%
 
-- 
cgit v1.2.3


From f6b22fd533bd61e9dbcb6374295df321de99b1f2 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 23 Sep 2024 03:05:41 +0200
Subject: Abgabe

---
 library/algebra/group.tex                   |  2 +-
 library/algebra/monoid.tex                  |  2 +-
 library/cardinal.tex                        |  2 +-
 library/numbers.tex                         |  2 +-
 library/topology/basis.tex                  |  2 +-
 library/topology/continuous.tex             |  2 ++
 library/topology/metric-space.tex           |  4 ++--
 library/topology/real-topological-space.tex |  2 +-
 library/topology/separation.tex             |  2 ++
 library/topology/topological-space.tex      |  2 +-
 library/topology/urysohn.tex                |  4 ++--
 library/topology/urysohn2.tex               | 18 ++++++++++++++----
 12 files changed, 29 insertions(+), 15 deletions(-)

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

diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index 7de1051..449bacb 100644
--- a/library/algebra/group.tex
+++ b/library/algebra/group.tex
@@ -1,5 +1,5 @@
 \import{algebra/monoid.tex}
-\section{Group}
+\section{Group}\label{form_sec_group}
 
 \begin{struct}\label{group}
     A group $G$ is a monoid such that
diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex
index 06fcb50..3249a93 100644
--- a/library/algebra/monoid.tex
+++ b/library/algebra/monoid.tex
@@ -1,5 +1,5 @@
 \import{algebra/semigroup.tex}
-\section{Monoid}
+\section{Monoid}\label{form_sec_monoid}
 
 \begin{struct}\label{monoid}
     A monoid $A$ is a semigroup equipped with
diff --git a/library/cardinal.tex b/library/cardinal.tex
index 044e5d1..5682619 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -1,4 +1,4 @@
-\section{Cardinality}
+\section{Cardinality}\label{form_sec_cardinality}
 
 \import{set.tex}
 \import{ordinal.tex}
diff --git a/library/numbers.tex b/library/numbers.tex
index ac0a683..d3af3f1 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -4,7 +4,7 @@
 \import{ordinal.tex}
 
 
-\section{The real numbers}
+\section{The numbers}\label{form_sec_numbers}
 
 \begin{signature}
     $\reals$ is a set.
diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index 052c551..f0f77e4 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -2,7 +2,7 @@
 \import{set.tex}
 \import{set/powerset.tex}
 
-\subsection{Topological basis}
+\subsection{Topological basis}\label{form_sec_topobasis}
 
 \begin{abbreviation}\label{covers}
     $C$ covers $X$ iff
diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex
index a9bc58e..95c4d0a 100644
--- a/library/topology/continuous.tex
+++ b/library/topology/continuous.tex
@@ -3,6 +3,8 @@
 \import{function.tex}
 \import{set.tex}
 
+\subsection{Continuous}\label{form_sec_continuous}
+
 \begin{definition}\label{continuous}
     $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$.
 \end{definition}
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index 0ed7bab..031aa0f 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -4,10 +4,10 @@
 \import{set/powerset.tex}
 \import{topology/basis.tex}
 
-\section{Metric Spaces}
+\section{Metric Spaces}\label{form_sec_metric}
 
 \begin{definition}\label{metric}
-    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reaaals$ and
+    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and
     for all $x,y,z \in M$ we have 
         $f(x,x) = \zero$ and 
         $f(x,y) = f(y,x)$ and
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index c76fd46..db7ee94 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -11,7 +11,7 @@
 \import{function.tex}
 
 
-\section{Topology Reals}
+\section{Topology Reals}\label{form_sec_toporeals}
 
 \begin{definition}\label{topological_basis_reals_eps_ball}
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index 0c68290..aaa3907 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -1,6 +1,8 @@
 \import{topology/topological-space.tex}
 \import{set.tex}
 
+\subsection{Separation}\label{form_sec_separation}
+
 % T0 separation
 \begin{definition}\label{is_kolmogorov}
     $X$ is Kolmogorov iff
diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index f8bcb93..409e107 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -2,7 +2,7 @@
 \import{set/powerset.tex}
 \import{set/cons.tex}
 
-\section{Topological spaces}
+\section{Topological spaces}\label{form_sec_topospaces}
 
 \begin{struct}\label{topological_space}
     A topological space $X$ is a onesorted structure equipped with
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index ae03273..cd85fbc 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -13,7 +13,7 @@
 \import{set/fixpoint.tex}
 \import{set/product.tex}
 
-\section{Urysohns Lemma}
+\section{Urysohns Lemma Part 1 with struct}\label{form_sec_urysohn1}
 %           In this section we want to proof Urysohns lemma. 
 %           We try to follow the proof of Klaus Jänich in his book. TODO: Book reference
 %           The Idea is to construct staircase functions as a chain.
@@ -22,7 +22,7 @@
 
 %Chains of  sets.
 
-The first tept will be a formalisation of chain constructions.
+This is the first attempt to prove Urysohns Lemma with the usage of struct. 
 
 \subsection{Chains of sets}
 %           Assume $A,B$ are subsets of a topological space $X$.
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 08841da..a1a3ba0 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -15,7 +15,7 @@
 \import{topology/real-topological-space.tex}
 \import{set/equinumerosity.tex}
 
-\section{Urysohns Lemma}
+\section{Urysohns Lemma}\label{form_sec_urysohn}
 
 
 
@@ -891,15 +891,25 @@
             \begin{byCase}
                 \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.}
                     Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$.
-                    Therefore $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    We show that $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    \begin{subproof}
+                        Omitted.
+                    \end{subproof}
                     Therefore $x \notin  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.
-                    Then $g(x) = 1$ .
+                    We show that $g(x) = 1$.
+                    \begin{subproof}
+                        Omitted.
+                    \end{subproof}
                 \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.}
                     \begin{byCase}
                         \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.}
-                            $g(x) = \zero$.
+                            We show that $g(x) = \zero$.
+                            \begin{subproof}
+                                Omitted.
+                            \end{subproof}
                         \caseOf{$x \in  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.}
                             Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$.
+                            Omitted.
                     \end{byCase}
             \end{byCase}
 
-- 
cgit v1.2.3

