diff --git a/Bookshelf/Apostol.tex b/Bookshelf/Apostol.tex index 857ddc0..eaf3b47 100644 --- a/Bookshelf/Apostol.tex +++ b/Bookshelf/Apostol.tex @@ -7,6 +7,7 @@ \graphicspath{{./Apostol/images/}} \newcommand{\lean}[2]{\leanref{../#1.html\##2}{#2}} +\newcommand{\leanPretty}[3]{\leanref{../#1.html\##2}{#3}} \begin{document} @@ -26,7 +27,7 @@ Nonempty set $S$ has supremum $L$ if and only if set $-S$ has infimum $-L$. \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.is\_lub\_neg\_set\_iff\_is\_glb\_set\_neg} \divider @@ -48,7 +49,7 @@ Every nonempty set $S$ that is bounded below has a greatest lower bound; that \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.exists\_isGLB} \divider @@ -68,7 +69,7 @@ For every real $x$ there exists a positive integer $n$ such that $n > x$. \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.exists\_pnat\_geq\_self} \divider @@ -92,7 +93,7 @@ If $x > 0$ and if $y$ is an arbitrary real number, there exists a positive \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.exists\_pnat\_mul\_self\_geq\_of\_pos} \divider @@ -112,7 +113,7 @@ If three real numbers $a$, $x$, and $y$ satisfy the inequalities \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.forall\_pnat\_leq\_self\_leq\_frac\_imp\_eq} \divider @@ -156,7 +157,7 @@ If three real numbers $a$, $x$, and $y$ satisfy the inequalities \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.forall\_pnat\_frac\_leq\_self\_leq\_imp\_eq} \divider @@ -204,7 +205,7 @@ If $S$ has a supremum, then for some $x$ in $S$ we have $x > \sup{S} - h$. \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.sup\_imp\_exists\_gt\_sup\_sub\_delta} \divider @@ -227,7 +228,7 @@ If $S$ has an infimum, then for some $x$ in $S$ we have $x < \inf{S} + h$. \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.inf\_imp\_exists\_lt\_inf\_add\_delta} \divider @@ -259,7 +260,7 @@ If each of $A$ and $B$ has a supremum, then $C$ has a supremum, and \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.sup\_minkowski\_sum\_eq\_sup\_add\_sup} \divider @@ -328,7 +329,7 @@ If each of $A$ and $B$ has an infimum, then $C$ has an infimum, and \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.inf\_minkowski\_sum\_eq\_inf\_add\_inf} \divider @@ -398,7 +399,7 @@ Given two nonempty subsets $S$ and $T$ of $\mathbb{R}$ such that $$s \leq t$$ \begin{proof} - \lean{Chapter\_I\_03} + \lean{Bookshelf/Apostol/Chapter\_I\_03} {Apostol.Chapter\_I\_03.forall\_mem\_le\_forall\_mem\_imp\_sup\_le\_inf} \divider @@ -436,7 +437,8 @@ For each set $S$ in $\mathscr{M}$, we have $a(S) \geq 0$. \begin{axiom} - \lean{Common/Real/Geometry/Area}{Nonnegative-Property} + \leanPretty{Common/Real/Geometry/Area}{Nonnegative-Property} + {Nonnegative Property} \end{axiom} @@ -448,7 +450,8 @@ If $S$ and $T$ are in $\mathscr{M}$, then $S \cup T$ and $S \cap T$ are in \begin{axiom} - \lean{Common/Real/Geometry/Area}{Additive-Property} + \leanPretty{Common/Real/Geometry/Area}{Additive-Property} + {Additive Property} \end{axiom} @@ -460,7 +463,8 @@ If $S$ and $T$ are in $\mathscr{M}$ with $S \subseteq T$, then $T - S$ is in \begin{axiom} - \lean{Common/Real/Geometry/Area}{Difference-Property} + \leanPretty{Common/Real/Geometry/Area}{Difference-Property} + {Difference Property} \end{axiom} @@ -472,7 +476,8 @@ If a set $S$ is in $\mathscr{M}$ and if $T$ is congruent to $S$, then $T$ is \begin{axiom} - \lean{Common/Real/Geometry/Area}{Invariance-Under-Congruence} + \leanPretty{Common/Real/Geometry/Area}{Invariance-Under-Congruence} + {Invariance Under Congruence} \end{axiom} @@ -484,7 +489,8 @@ If the edges of $R$ have lengths $h$ and $k$, then $a(R) = hk$. \begin{axiom} - \lean{Common/Real/Geometry/Area}{Choice-of-Scale} + \leanPretty{Common/Real/Geometry/Area}{Choice-of-Scale} + {Choice of Scale} \end{axiom} @@ -503,7 +509,8 @@ If there is one and only one number $c$ which satisfies the inequalities \begin{axiom} - \lean{Common/Real/Geometry/Area}{Exhaustion-Property} + \leanPretty{Common/Real/Geometry/Area}{Exhaustion-Property} + {Exhaustion Property} \end{axiom} diff --git a/Bookshelf/Enderton.tex b/Bookshelf/Enderton.tex new file mode 100644 index 0000000..7b4e156 --- /dev/null +++ b/Bookshelf/Enderton.tex @@ -0,0 +1,36 @@ +\documentclass{report} + +\input{../preamble} + +\newcommand{\lean}[2]{\leanref{../#1.html\##2}{#2}} +\newcommand{\leanPretty}[3]{\leanref{../#1.html\##2}{#3}} + +\begin{document} + +\header + {A Mathematical Introduction to Logic} + {Herbert B. Enderton} + +\tableofcontents + +% Sets first chapter to `0` to match Enderton book. +\setcounter{chapter}{0} +\addtocounter{chapter}{-1} + +\chapter{Useful Facts About Sets}% +\label{chap:useful-facts-about-sets} + +\section{\unverified{Lemma 0A}}% +\label{sec: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$. + +\begin{proof} + + \lean{Bookshelf/Enderton/Chapter\_0}{Enderton.Chapter\_0.lemma\_0a} + +\end{proof} + +\end{document} diff --git a/Bookshelf/Enderton/Chapter_0.tex b/Bookshelf/Enderton/Chapter_0.tex deleted file mode 100644 index 6fa198c..0000000 --- a/Bookshelf/Enderton/Chapter_0.tex +++ /dev/null @@ -1,26 +0,0 @@ -\documentclass{article} - -\input{../../preamble} - -\newcommand{\lean}[1]{\leanref - {./Chapter\_0.html\#Enderton.Chapter\_0.#1} - {Enderton.Chapter\_0.#1}} - -\begin{document} - -\header{Useful Facts About Sets}{Herbert B. Enderton} - -\section*{\unverified{Lemma 0A}}% -\label{sec: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$. - -\begin{proof} - - \lean{lemma\_0a} - -\end{proof} - -\end{document} diff --git a/Common/Real/Sequence.tex b/Common/Real/Sequence.tex new file mode 100644 index 0000000..06f4fa1 --- /dev/null +++ b/Common/Real/Sequence.tex @@ -0,0 +1,44 @@ +\documentclass{article} + +\input{../../preamble} + +\newcommand{\lean}[2]{\leanref{../../#1.html\##2}{#2}} + +\begin{document} + +\header{Sequences}{} + +\tableofcontents + +\section{Summations}% +\label{sec:summations} + +\subsection{\unverified{Arithmetic Series}}% +\label{sub:sum-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}.$$ + +\begin{proof} + + \lean{Common/Real/Sequence/Arithmetic} + {Real.Arithmetic.sum\_recursive\_closed} + +\end{proof} + +\subsection{\unverified{Geometric Series}}% +\label{sub:sum-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}.$$ + +\begin{proof} + + \lean{Common/Real/Sequence/Geometric} + {Real.Geometric.sum\_recursive\_closed} + +\end{proof} + +\end{document} diff --git a/Common/Real/Sequence/Arithmetic.tex b/Common/Real/Sequence/Arithmetic.tex deleted file mode 100644 index c782c03..0000000 --- a/Common/Real/Sequence/Arithmetic.tex +++ /dev/null @@ -1,24 +0,0 @@ -\documentclass{article} - -\input{../../../preamble} - -\newcommand{\lean}[1]{\leanref - {./Arithmetic.html\#Real.Arithmetic.#1} - {Real.Arithmetic.#1}} - -\begin{document} - -\section{\unverified{Sum of Arithmetic Series}}% -\label{sec:sum-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}.$$ - -\begin{proof} - - \lean{sum\_recursive\_closed} - -\end{proof} - -\end{document} diff --git a/Common/Real/Sequence/Geometric.tex b/Common/Real/Sequence/Geometric.tex deleted file mode 100644 index 83db8b9..0000000 --- a/Common/Real/Sequence/Geometric.tex +++ /dev/null @@ -1,24 +0,0 @@ -\documentclass{article} - -\input{../../../preamble} - -\newcommand{\lean}[1]{\leanref - {./Geometric.html\#Real.Geometric.#1} - {Real.Geometric.#1}} - -\begin{document} - -\section{\unverified{Sum of Geometric Series}}% -\label{sec:sum-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}.$$ - -\begin{proof} - - \lean{sum\_recursive\_closed} - -\end{proof} - -\end{document}