From 418103eb8c4b9dfd9d5bfc0e364c7483f5da008f Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 10 Apr 2023 16:25:32 -0600 Subject: [PATCH] I_3_11 Apostol. Tex proof. Also nest paragraphs in LaTeX structures. --- common/Common/Sequence/Arithmetic.tex | 8 ++-- common/Common/Sequence/Geometric.tex | 8 ++-- .../Enderton/Chapter0.tex | 6 +-- one-variable-calculus/Apostol/Chapter_I_3.tex | 47 ++++++++++++++----- 4 files changed, 47 insertions(+), 22 deletions(-) diff --git a/common/Common/Sequence/Arithmetic.tex b/common/Common/Sequence/Arithmetic.tex index 015ead2..70953bd 100644 --- a/common/Common/Sequence/Arithmetic.tex +++ b/common/Common/Sequence/Arithmetic.tex @@ -6,15 +6,15 @@ \begin{theorem}[Sum of Arithmetic Series] -Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$. -Then for some $n \in \mathbb{N}$, -$$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$ + Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$. + Then for some $n \in \mathbb{N}$, + $$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$ \end{theorem} \begin{proof} -\href{Arithmetic.lean}{Common.Sequence.Arithmetic.sum_recursive_closed} + \href{Arithmetic.lean}{Common.Sequence.Arithmetic.sum_recursive_closed} \end{proof} diff --git a/common/Common/Sequence/Geometric.tex b/common/Common/Sequence/Geometric.tex index 68182fb..d0ac39b 100644 --- a/common/Common/Sequence/Geometric.tex +++ b/common/Common/Sequence/Geometric.tex @@ -6,15 +6,15 @@ \begin{theorem}[Sum of Geometric Series] -Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$. -Then for some $n \in \mathbb{N}$, -$$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$ + Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$. + Then for some $n \in \mathbb{N}$, + $$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$ \end{theorem} \begin{proof} -\href{Geometric.lean}{Common.Sequence.Geometric.sum_recursive_closed} + \href{Geometric.lean}{Common.Sequence.Geometric.sum_recursive_closed} \end{proof} diff --git a/mathematical-introduction-logic/Enderton/Chapter0.tex b/mathematical-introduction-logic/Enderton/Chapter0.tex index b27461a..5de3d0d 100644 --- a/mathematical-introduction-logic/Enderton/Chapter0.tex +++ b/mathematical-introduction-logic/Enderton/Chapter0.tex @@ -6,14 +6,14 @@ \begin{theorem}[Lemma 0A] -Assume that $\langle x_1, \ldots, x_m \rangle = \langle y_1, \ldots, y_m, \ldots, y_{m+k} \rangle$. -Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$. + Assume that $\langle x_1, \ldots, x_m \rangle = \langle y_1, \ldots, y_m, \ldots, y_{m+k} \rangle$. + Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$. \end{theorem} \begin{proof} -\href{Chapter0.lean}{Enderton.Chapter0.lemma_0a} + \href{Chapter0.lean}{Enderton.Chapter0.lemma_0a} \end{proof} diff --git a/one-variable-calculus/Apostol/Chapter_I_3.tex b/one-variable-calculus/Apostol/Chapter_I_3.tex index ec4706e..1591b8d 100644 --- a/one-variable-calculus/Apostol/Chapter_I_3.tex +++ b/one-variable-calculus/Apostol/Chapter_I_3.tex @@ -1,4 +1,5 @@ \documentclass{article} +\usepackage[shortlabels]{enumitem} \input{../../common/preamble} @@ -6,52 +7,76 @@ \begin{xtheorem}{I.27} -Every nonempty set $S$ that is bounded below has a greatest lower bound; -that is, there is a real number $L$ such that $L = \inf{S}$. + Every nonempty set $S$ that is bounded below has a greatest lower bound; that + is, there is a real number $L$ such that $L = \inf{S}$. \end{xtheorem} \begin{proof} -\href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.exists_isGLB} + \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.exists_isGLB} \end{proof} \begin{xtheorem}{I.29} -For every real $x$ there exists a positive integer $n$ such that $n > x$. + For every real $x$ there exists a positive integer $n$ such that $n > x$. \end{xtheorem} \begin{proof} -\href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.exists_pnat_geq_self} + \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.exists_pnat_geq_self} \end{proof} \begin{xtheorem}{I.30}[Archimedean Property of the Reals] -If $x > 0$ and if $y$ is an arbitrary real number, there exists a positive integer $n$ such that $nx > y$. + If $x > 0$ and if $y$ is an arbitrary real number, there exists a positive + integer $n$ such that $nx > y$. \end{xtheorem} \begin{proof} -\href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.exists_pnat_mul_self_geq_of_pos} + \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.exists_pnat_mul_self_geq_of_pos} \end{proof} \begin{xtheorem}{I.31} -If three real numbers $a$, $x$, and $y$ satisfy the inequalities -$$a \leq x \leq a + \frac{y}{n}$$ -for every integer $n \geq 1$, then $x = a$. + If three real numbers $a$, $x$, and $y$ satisfy the inequalities + $$a \leq x \leq a + \frac{y}{n}$$ + for every integer $n \geq 1$, then $x = a$. \end{xtheorem} \begin{proof} -\href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.forall_pnat_leq_self_leq_frac_imp_eq} + \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.forall_pnat_leq_self_leq_frac_imp_eq} + +\end{proof} + +\begin{xtheorem}{I.32} + + Let $h$ be a given positive number and let $S$ be a set of real numbers. + \begin{enumerate}[(a)] + \item If $S$ has a supremum, then for some $x$ in $S$ we have + $$x > \sup{S} - h.$$ + \item If $S$ has an infimum, then for some $x$ in $S$ we have + $$x < \inf{S} + h.$$ + \end{enumerate} + +\end{xtheorem} + +\begin{proof} + + \ % Force space prior to *Proof.* + + \begin{enumerate}[(a)] + \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.arb_close_to_sup} + \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.arb_close_to_inf} + \end{enumerate} \end{proof}