diff options
| -rw-r--r-- | library/numbers.tex | 3 | ||||
| -rw-r--r-- | library/topology/real-topological-space.tex | 27 | ||||
| -rw-r--r-- | source/Syntax/Concrete.hs | 6 | ||||
| -rw-r--r-- | source/Syntax/Token.hs | 8 |
4 files changed, 25 insertions, 19 deletions
diff --git a/library/numbers.tex b/library/numbers.tex index 406553e..ac0a683 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -613,6 +613,9 @@ Laws of the order on the reals \subsection{Order on the reals} +\begin{axiom}\label{reals_order_is_transitive} + For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$. +\end{axiom} \begin{lemma}\label{plus_one_order} diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex index e5e17ef..d9790aa 100644 --- a/library/topology/real-topological-space.tex +++ b/library/topology/real-topological-space.tex @@ -70,7 +70,7 @@ Then $\epsBall{x}{\epsilon}$ is inhabited. \end{lemma} \begin{proof} - $x < x + \epsilon$. + $x < x + \epsilon$ by \cref{reals_order_behavior_with_addition,realsplus,reals_axiom_zero_in_reals,reals_axiom_kommu,reals_axiom_zero}. $x - \epsilon < x$. $x \in \epsBall{x}{\epsilon}$. \end{proof} @@ -104,12 +104,8 @@ 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$. @@ -207,12 +203,16 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$. \end{lemma} +\begin{lemma}\label{one_in_realsplus} + $1 \in \realsplus$. +\end{lemma} + \begin{lemma}\label{reals_existence_addition_reverse} For all $\delta \in \reals$ there exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$. \end{lemma} \begin{proof} Fix $\delta \in \reals$. - Follows by \cref{reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}. + Follows by \cref{one_in_realsplus,reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}. \end{proof} \begin{lemma}\label{reals_addition_minus_behavior1} @@ -260,7 +260,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have \end{subproof} We show that $\epsBall{x}{\epsilon} \subseteq \intervalopen{a}{b}$. \begin{subproof} - It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$. + It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$ by \cref{subseteq}. Fix $y \in \epsBall{x}{\epsilon}$. \end{subproof} @@ -270,7 +270,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have Suppose $a,b,x,y \in \reals$. Suppose $a < b$. Suppose $x < y$. - If $a \leq x < y \leq b$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$. + Suppose $a \leq x < y \leq b$. + Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$. \end{lemma} \begin{proof} Omitted. @@ -280,7 +281,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have Suppose $a,b,x,y \in \reals$. Suppose $a < b$. Suppose $x < y$. - If $a = x$ and $b \leq y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$. + Suppose $a = x$ and $b \leq y$. + Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$. \end{lemma} \begin{proof} Omitted. @@ -290,7 +292,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have Suppose $a,b,x,y \in \reals$. Suppose $a < b$. Suppose $x < y$. - If $a \leq x$ and $b = y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$. + Suppose $a \leq x$ and $b = y$. + Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$. \end{lemma} \begin{proof} Omitted. diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 9d52995..7a89bea 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -373,15 +373,15 @@ grammar lexicon@Lexicon{..} = mdo -- 3 & \text{else} -- \end{cases} - functionDefineCase <- rule $ (,) <$> (_ampersand *> expr) <*> (_ampersand *> text _if *> formula) + functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula) defineFunctionMathy <- rule $ DefineFunctionMathy <$> (_define *> beginMath *> varSymbol) -- Define $ f <*> (_colon *> varSymbol) -- : 'var' \to 'var' <*> (_to *> expr <* endMath <* _suchThat) -- <*> (_suchThat *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula)))) -- <*> (_suchThat *> align (many1 (varSymbol <* exprApp <* formula))) - <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq <* endMath) - <*> cases (many1 functionDefineCase) + <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq ) + <*> cases (many1 functionDefineCase) <* endMath <* optional _dot <*> proof diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs index 52da86a..53e1e6a 100644 --- a/source/Syntax/Token.hs +++ b/source/Syntax/Token.hs @@ -189,7 +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@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:)) Just t -> goNormal (f . (t:)) goText f = do r <- optional textToken @@ -205,7 +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 = 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:)) @@ -282,7 +282,7 @@ alignBegin = guardM isTextMode *> lexeme do casesBegin :: Lexer (Located Token) casesBegin = guardM isTextMode *> lexeme do Char.string "\\begin{cases}" - setMathMode + --setMathMode pure (BeginEnv "cases") -- | Parses a single end math token. @@ -301,7 +301,7 @@ alignEnd = guardM isMathMode *> lexeme do casesEnd :: Lexer (Located Token) casesEnd = guardM isMathMode *> lexeme do Char.string "\\end{cases}" - setTextMode + --setTextMode pure (EndEnv "cases") |