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