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