diff --git a/Bookshelf/Real/Sequence.tex b/Bookshelf/Real/Sequence.tex deleted file mode 100644 index 4dfcc3d..0000000 --- a/Bookshelf/Real/Sequence.tex +++ /dev/null @@ -1,37 +0,0 @@ -\documentclass{article} - -\input{preamble} - -\newcommand{\ns}{Real} -\newcommand{\linkA}[1]{\href{../Sequence/Arithmetic.html\#\ns.#1}{\ns.#1}} -\newcommand{\linkG}[1]{\href{../Sequence/Geometric.html\#\ns.#1}{\ns.#1}} - -\begin{document} - -\section*{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} - - \linkA{Arithmetic.sum\_recursive\_closed} - -\end{proof} - -\section*{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} - - \linkG{Geometric.sum\_recursive\_closed} - -\end{proof} - -\end{document} diff --git a/Bookshelf/Real/Sequence/Arithmetic.tex b/Bookshelf/Real/Sequence/Arithmetic.tex new file mode 100644 index 0000000..5e3c044 --- /dev/null +++ b/Bookshelf/Real/Sequence/Arithmetic.tex @@ -0,0 +1,23 @@ +\documentclass{article} + +\input{preamble} + +\newcommand{\link}[1]{\lean{../../..}{Bookshelf/Real/Sequence/Arithmetic} + {Real.Arithmetic.#1}} + +\begin{document} + +\section*{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} + + \link{sum_recursive_closed} + +\end{proof} + +\end{document} diff --git a/Bookshelf/Real/Sequence/Geometric.tex b/Bookshelf/Real/Sequence/Geometric.tex new file mode 100644 index 0000000..e049c78 --- /dev/null +++ b/Bookshelf/Real/Sequence/Geometric.tex @@ -0,0 +1,23 @@ +\documentclass{article} + +\input{preamble} + +\newcommand{\link}[1]{\lean{../../..}{Bookshelf/Real/Sequence/Geometric} + {Real.Geometric.#1}} + +\begin{document} + +\section*{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} + + \link{sum_recursive_closed} + +\end{proof} + +\end{document} diff --git a/Exercises/Apostol/Chapter_I_3.tex b/Exercises/Apostol/Chapter_I_3.tex index deebe97..23b3a5b 100644 --- a/Exercises/Apostol/Chapter_I_3.tex +++ b/Exercises/Apostol/Chapter_I_3.tex @@ -3,8 +3,8 @@ \input{preamble} -\newcommand{\ns}{Exercises.Apostol.Chapter\_I\_3.Real} -\newcommand{\link}[1]{\href{../Chapter_I_3.html\#\ns.#1}{\ns.#1}} +\newcommand{\link}[1]{\lean{../..}{Exercises/Apostol/Chapter_I_3} + {Exercises.Apostol.Chapter\_I\_3.Real.#1}} \begin{document} @@ -16,7 +16,7 @@ is, there is a real number $L$ such that $L = \inf{S}$. \begin{proof} - \link{exists\_isGLB} + \link{exists_isGLB} \end{proof} @@ -27,7 +27,7 @@ For every real $x$ there exists a positive integer $n$ such that $n > x$. \begin{proof} - \link{exists\_pnat\_geq\_self} + \link{exists_pnat_geq_self} \end{proof} @@ -39,7 +39,7 @@ integer $n$ such that $nx > y$. \begin{proof} - \link{exists\_pnat\_mul\_self\_geq\_of\_pos} + \link{exists_pnat_mul_self_geq_of_pos} \end{proof} @@ -52,7 +52,7 @@ for every integer $n \geq 1$, then $x = a$. \begin{proof} - \link{forall\_pnat\_leq\_self\_leq\_frac\_imp\_eq} + \link{forall_pnat_leq_self_leq_frac_imp_eq} \end{proof} @@ -70,8 +70,8 @@ Let $h$ be a given positive number and let $S$ be a set of real numbers. \begin{proof} \begin{enumerate}[(a)] - \item \link{sup\_imp\_exists\_gt\_sup\_sub\_delta} - \item \link{inf\_imp\_exists\_lt\_inf\_add\_delta} + \item \link{sup_imp_exists_gt_sup_sub_delta} + \item \link{inf_imp_exists_lt_inf_add_delta} \end{enumerate} \end{proof} @@ -92,8 +92,8 @@ $$C = \{a + b : a \in A, b \in B\}.$$ \begin{proof} \begin{enumerate}[(a)] - \item \link{sup\_minkowski\_sum\_eq\_sup\_add\_sup} - \item \link{inf\_minkowski\_sum\_eq\_inf\_add\_inf} + \item \link{sup_minkowski_sum_eq_sup_add_sup} + \item \link{inf_minkowski_sum_eq_inf_add_inf} \end{enumerate} \end{proof} @@ -109,7 +109,7 @@ $$\sup{S} \leq \inf{T}.$$ \begin{proof} - \link{forall\_mem\_le\_forall\_mem\_imp\_sup\_le\_inf} + \link{forall_mem_le_forall_mem_imp_sup_le_inf} \end{proof} diff --git a/Exercises/Enderton/Chapter0.tex b/Exercises/Enderton/Chapter0.tex index 8a5a44d..e235dfd 100644 --- a/Exercises/Enderton/Chapter0.tex +++ b/Exercises/Enderton/Chapter0.tex @@ -2,8 +2,8 @@ \input{preamble} -\newcommand{\ns}{Exercises.Enderton.Chapter0} -\newcommand{\link}[1]{\href{../Chapter0.html\#\ns.#1}{\ns.#1}} +\newcommand{\link}[1]{\lean{../..}{Exercises/Enderton/Chapter0} + {Exercises.Enderton.Chapter0.#1}} \begin{document} @@ -15,7 +15,7 @@ Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$. \begin{proof} - \link{lemma\_0a} + \link{lemma_0a} \end{proof} diff --git a/preamble.tex b/preamble.tex index 1354b8a..6383a56 100644 --- a/preamble.tex +++ b/preamble.tex @@ -1,6 +1,6 @@ \usepackage{amsfonts, amsthm} +\usepackage[T1]{fontenc} \usepackage{hyperref} -\usepackage{underscore} \newtheorem{theorem}{Theorem} \newtheorem{xtheoreminner}{Theorem} @@ -10,3 +10,14 @@ }{\endxtheoreminner} \hypersetup{colorlinks=true, urlcolor=blue} + +% https://tex.stackexchange.com/a/232188 +\newcommand{\startunderscoreletter}{\catcode`_ 12\relax} +\newcommand{\stopunderscoreletter}{\catcode`_ 8\relax} + +% The first argument refers to a relative path upward from a current file to +% the root of the workspace (i.e. where this `preamble.tex` file is located). +% We include an additional nesting of `..` to account for the generated `LaTeX` +% directory automatically included when generating documentation. +\newcommand{\lean}[3]{\href{#1/../#2.html\##3}{ + \startunderscoreletter #3 \stopunderscoreletter}}