r
/
bookshelf
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

I_3_11 Apostol. Tex proof. 

Also nest paragraphs in LaTeX structures.
finite-set-exercises
Joshua Potter 2023-04-10 16:25:32 -06:00
parent a2b138233a
commit 418103eb8c
4 changed files with 47 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
common/Common/Sequence/Arithmetic.tex
View File

@ -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}

8
common/Common/Sequence/Geometric.tex
View File

@ -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}

6
mathematical-introduction-logic/Enderton/Chapter0.tex
View File

@ -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}

47
one-variable-calculus/Apostol/Chapter_I_3.tex
View File

@ -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}