Perform same aggregation on Enderton and Sequence tex files.
parent
e7e657950b
commit
ddcb0f9717
|
@ -7,6 +7,7 @@
|
||||||
\graphicspath{{./Apostol/images/}}
|
\graphicspath{{./Apostol/images/}}
|
||||||
|
|
||||||
\newcommand{\lean}[2]{\leanref{../#1.html\##2}{#2}}
|
\newcommand{\lean}[2]{\leanref{../#1.html\##2}{#2}}
|
||||||
|
\newcommand{\leanPretty}[3]{\leanref{../#1.html\##2}{#3}}
|
||||||
|
|
||||||
\begin{document}
|
\begin{document}
|
||||||
|
|
||||||
|
@ -26,7 +27,7 @@ Nonempty set $S$ has supremum $L$ if and only if set $-S$ has infimum $-L$.
|
||||||
|
|
||||||
\begin{proof}
|
\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}
|
{Apostol.Chapter\_I\_03.is\_lub\_neg\_set\_iff\_is\_glb\_set\_neg}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -48,7 +49,7 @@ Every nonempty set $S$ that is bounded below has a greatest lower bound; that
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
||||||
\lean{Chapter\_I\_03}
|
\lean{Bookshelf/Apostol/Chapter\_I\_03}
|
||||||
{Apostol.Chapter\_I\_03.exists\_isGLB}
|
{Apostol.Chapter\_I\_03.exists\_isGLB}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -68,7 +69,7 @@ For every real $x$ there exists a positive integer $n$ such that $n > x$.
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
||||||
\lean{Chapter\_I\_03}
|
\lean{Bookshelf/Apostol/Chapter\_I\_03}
|
||||||
{Apostol.Chapter\_I\_03.exists\_pnat\_geq\_self}
|
{Apostol.Chapter\_I\_03.exists\_pnat\_geq\_self}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -92,7 +93,7 @@ If $x > 0$ and if $y$ is an arbitrary real number, there exists a positive
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
||||||
\lean{Chapter\_I\_03}
|
\lean{Bookshelf/Apostol/Chapter\_I\_03}
|
||||||
{Apostol.Chapter\_I\_03.exists\_pnat\_mul\_self\_geq\_of\_pos}
|
{Apostol.Chapter\_I\_03.exists\_pnat\_mul\_self\_geq\_of\_pos}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -112,7 +113,7 @@ If three real numbers $a$, $x$, and $y$ satisfy the inequalities
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
||||||
\lean{Chapter\_I\_03}
|
\lean{Bookshelf/Apostol/Chapter\_I\_03}
|
||||||
{Apostol.Chapter\_I\_03.forall\_pnat\_leq\_self\_leq\_frac\_imp\_eq}
|
{Apostol.Chapter\_I\_03.forall\_pnat\_leq\_self\_leq\_frac\_imp\_eq}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -156,7 +157,7 @@ If three real numbers $a$, $x$, and $y$ satisfy the inequalities
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
||||||
\lean{Chapter\_I\_03}
|
\lean{Bookshelf/Apostol/Chapter\_I\_03}
|
||||||
{Apostol.Chapter\_I\_03.forall\_pnat\_frac\_leq\_self\_leq\_imp\_eq}
|
{Apostol.Chapter\_I\_03.forall\_pnat\_frac\_leq\_self\_leq\_imp\_eq}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -204,7 +205,7 @@ If $S$ has a supremum, then for some $x$ in $S$ we have $x > \sup{S} - h$.
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
||||||
\lean{Chapter\_I\_03}
|
\lean{Bookshelf/Apostol/Chapter\_I\_03}
|
||||||
{Apostol.Chapter\_I\_03.sup\_imp\_exists\_gt\_sup\_sub\_delta}
|
{Apostol.Chapter\_I\_03.sup\_imp\_exists\_gt\_sup\_sub\_delta}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -227,7 +228,7 @@ If $S$ has an infimum, then for some $x$ in $S$ we have $x < \inf{S} + h$.
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
||||||
\lean{Chapter\_I\_03}
|
\lean{Bookshelf/Apostol/Chapter\_I\_03}
|
||||||
{Apostol.Chapter\_I\_03.inf\_imp\_exists\_lt\_inf\_add\_delta}
|
{Apostol.Chapter\_I\_03.inf\_imp\_exists\_lt\_inf\_add\_delta}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -259,7 +260,7 @@ If each of $A$ and $B$ has a supremum, then $C$ has a supremum, and
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
||||||
\lean{Chapter\_I\_03}
|
\lean{Bookshelf/Apostol/Chapter\_I\_03}
|
||||||
{Apostol.Chapter\_I\_03.sup\_minkowski\_sum\_eq\_sup\_add\_sup}
|
{Apostol.Chapter\_I\_03.sup\_minkowski\_sum\_eq\_sup\_add\_sup}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -328,7 +329,7 @@ If each of $A$ and $B$ has an infimum, then $C$ has an infimum, and
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
||||||
\lean{Chapter\_I\_03}
|
\lean{Bookshelf/Apostol/Chapter\_I\_03}
|
||||||
{Apostol.Chapter\_I\_03.inf\_minkowski\_sum\_eq\_inf\_add\_inf}
|
{Apostol.Chapter\_I\_03.inf\_minkowski\_sum\_eq\_inf\_add\_inf}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -398,7 +399,7 @@ Given two nonempty subsets $S$ and $T$ of $\mathbb{R}$ such that $$s \leq t$$
|
||||||
|
|
||||||
\begin{proof}
|
\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}
|
{Apostol.Chapter\_I\_03.forall\_mem\_le\_forall\_mem\_imp\_sup\_le\_inf}
|
||||||
|
|
||||||
\divider
|
\divider
|
||||||
|
@ -436,7 +437,8 @@ For each set $S$ in $\mathscr{M}$, we have $a(S) \geq 0$.
|
||||||
|
|
||||||
\begin{axiom}
|
\begin{axiom}
|
||||||
|
|
||||||
\lean{Common/Real/Geometry/Area}{Nonnegative-Property}
|
\leanPretty{Common/Real/Geometry/Area}{Nonnegative-Property}
|
||||||
|
{Nonnegative Property}
|
||||||
|
|
||||||
\end{axiom}
|
\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}
|
\begin{axiom}
|
||||||
|
|
||||||
\lean{Common/Real/Geometry/Area}{Additive-Property}
|
\leanPretty{Common/Real/Geometry/Area}{Additive-Property}
|
||||||
|
{Additive Property}
|
||||||
|
|
||||||
\end{axiom}
|
\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}
|
\begin{axiom}
|
||||||
|
|
||||||
\lean{Common/Real/Geometry/Area}{Difference-Property}
|
\leanPretty{Common/Real/Geometry/Area}{Difference-Property}
|
||||||
|
{Difference Property}
|
||||||
|
|
||||||
\end{axiom}
|
\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}
|
\begin{axiom}
|
||||||
|
|
||||||
\lean{Common/Real/Geometry/Area}{Invariance-Under-Congruence}
|
\leanPretty{Common/Real/Geometry/Area}{Invariance-Under-Congruence}
|
||||||
|
{Invariance Under Congruence}
|
||||||
|
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
|
|
||||||
|
@ -484,7 +489,8 @@ If the edges of $R$ have lengths $h$ and $k$, then $a(R) = hk$.
|
||||||
|
|
||||||
\begin{axiom}
|
\begin{axiom}
|
||||||
|
|
||||||
\lean{Common/Real/Geometry/Area}{Choice-of-Scale}
|
\leanPretty{Common/Real/Geometry/Area}{Choice-of-Scale}
|
||||||
|
{Choice of Scale}
|
||||||
|
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
|
|
||||||
|
@ -503,7 +509,8 @@ If there is one and only one number $c$ which satisfies the inequalities
|
||||||
|
|
||||||
\begin{axiom}
|
\begin{axiom}
|
||||||
|
|
||||||
\lean{Common/Real/Geometry/Area}{Exhaustion-Property}
|
\leanPretty{Common/Real/Geometry/Area}{Exhaustion-Property}
|
||||||
|
{Exhaustion Property}
|
||||||
|
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
|
|
||||||
|
|
|
@ -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}
|
|
@ -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}
|
|
|
@ -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}
|
|
@ -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}
|
|
|
@ -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}
|
|
Loading…
Reference in New Issue