diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-09-04 15:17:50 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-09-04 15:17:50 +0200 |
| commit | 68716d1ab46dee3dfc1b03089f941dbb6883cdcd (patch) | |
| tree | 7539b439e1407b8ec02a97006adfd039b12c9ccf /library/topology/real-topological-space.tex | |
| parent | c57360cf062805c86fed5d1f3f4adbf52c05f9ff (diff) | |
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")]]))
Diffstat (limited to 'library/topology/real-topological-space.tex')
| -rw-r--r-- | library/topology/real-topological-space.tex | 26 |
1 files changed, 26 insertions, 0 deletions
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 |