Add start of Enderton's "Elements of Set Theory."

Bookshelf.lean

@@ -1,4 +1,5 @@
 import Bookshelf.Apostol
 import Bookshelf.Avigad
-import Bookshelf.Enderton_Logic
+import Bookshelf.Enderton.Logic
+import Bookshelf.Enderton.Set
 import Bookshelf.Fraleigh

Bookshelf/Enderton/Logic.lean

@@ -0,0 +1 @@
+import Bookshelf.Enderton.Logic.Chapter_0

Bookshelf/Enderton/Logic.tex

@@ -1,7 +1,7 @@
 \documentclass{report}
 
-\input{../preamble}
+\input{../../preamble}
-\makeleancommands
+\makeleancommands{../..}
 
 \begin{document}
 

Bookshelf/Enderton/Logic/Chapter_0.lean

@@ -0,0 +1,10 @@
+/-! # Enderton.Logic.Chapter_0
+
+Useful Facts About Sets
+-/
+
+namespace Enderton.Logic.Chapter_0
+
+-- TODO
+
+end Enderton.Logic.Chapter_0

Bookshelf/Enderton/Set.lean

@@ -0,0 +1 @@
+import Bookshelf.Enderton.Set.Chapter_1

Bookshelf/Enderton/Set.tex

@@ -0,0 +1,190 @@
+\documentclass{report}
+
+\input{../../preamble}
+\makeleancommands{../..}
+
+\begin{document}
+
+\header{Elements of Set Theory}{Herbert B. Enderton}
+
+\tableofcontents
+
+\begingroup
+\renewcommand\thechapter{R}
+\setcounter{chapter}{0}
+\addtocounter{chapter}{-1}
+
+\chapter{Reference}%
+\label{chap:reference}
+
+\section{\defined{Powerset}}%
+\label{ref:powerset}
+
+The \textbf{powerset} of some set $A$ is the set of all subsets of $A$.
+
+\begin{definition}
+
+  \lean{Mathlib/Init/Set}{Set.powerset}
+
+\end{definition}
+
+\section{\defined{Principle of Extensionality}}%
+\label{ref:principle-extensionality}
+
+If $A$ and $B$ are sets such that for every object $t$,
+  $$t \in A \quad\text{iff}\quad t \in B,$$
+  then $A = B$.
+
+\begin{axiom}
+
+  \lean{Mathlib/Init/Set}{Set.ext}
+
+\end{axiom}
+
+\endgroup
+
+\chapter{Introduction}%
+\label{chap:introduction}
+
+\section{Baby Set Theory}%
+\label{sec:baby-set-theory}
+
+\subsection{\partial{Exercise 1}}%
+\label{sub:baby-set-theory-1}
+
+Which of the following become true when "$\in$" is inserted in place of the
+  blank?
+Which become true when "$\subseteq$" is inserted?
+
+\subsubsection{\partial{Exercise 1a}}%
+\label{ssub:baby-set-theory-1a}
+
+$\{\emptyset\} \_\_\_\_ \{\emptyset, \{\emptyset\}\}$.
+
+\begin{proof}
+
+  Because the \textit{object} $\{\emptyset\}$ is a member of the right-hand set,
+    the statement is \textbf{true} in the case of "$\in$".
+
+  Because the \textit{members} of $\{\emptyset\}$ are all members of the
+    right-hand set, the statement is also \textbf{true} in the case of
+    "$\subseteq$".
+
+\end{proof}
+
+\subsubsection{\partial{Exercise 1b}}%
+\label{ssub:baby-set-theory-1b}
+
+$\{\emptyset\} \_\_\_\_ \{\emptyset, \{\{\emptyset\}\}\}$.
+
+\begin{proof}
+
+  Because the \textit{object} $\{\emptyset\}$ is not a member of the right-hand
+    set, the statement is \textbf{false} in the case of "$\in$".
+
+  Because the \textit{members} of $\{\emptyset\}$ are all members of the
+    right-hand set, the statement is \textbf{true} in the case of "$\subseteq$".
+
+\end{proof}
+
+\subsubsection{\partial{Exercise 1c}}%
+\label{ssub:baby-set-theory-1c}
+
+$\{\{\emptyset\}\} \_\_\_\_ \{\emptyset, \{\emptyset\}\}$.
+
+\begin{proof}
+
+  Because the \textit{object} $\{\{\emptyset\}\}$ is not a member of the
+    right-hand set, the statement is \textbf{false} in the case of "$\in$".
+
+  Because the \textit{members} of $\{\{\emptyset\}\}$ are all members of the
+    right-hand set, the statement is \textbf{true} in the case of "$\subseteq$".
+
+\end{proof}
+
+\subsubsection{\partial{Exercise 1d}}%
+\label{ssub:baby-set-theory-1d}
+
+$\{\{\emptyset\}\} \_\_\_\_ \{\emptyset, \{\{\emptyset\}\}\}$.
+
+\begin{proof}
+
+  Because the \textit{object} $\{\{\emptyset\}\}$ is a member of the right-hand
+    set, the statement is \textbf{true} in the case of "$\in$".
+
+  Because the \textit{members} of $\{\{\emptyset\}\}$ are not all members of the
+    right-hand set, the statement is \textbf{false} in the case of
+    "$\subseteq$".
+
+\end{proof}
+
+\subsubsection{\partial{Exercise 1e}}%
+\label{ssub:baby-set-theory-1e}
+
+$\{\{\emptyset\}\} \_\_ \{\emptyset, \{\emptyset, \{\emptyset\}\}\}$.
+
+\begin{proof}
+
+  Because the \textit{object} $\{\{\emptyset\}\}$ is not a member of the
+    right-hand set, the statement is \textbf{false} in the case of "$\in$".
+
+  Because the \textit{members} of $\{\{\emptyset\}\}$ are not all members of the
+    right-hand set, the statement is \textbf{false} in the case of
+    "$\subseteq$".
+
+\end{proof}
+
+\subsection{\partial{Exercise 2}}%
+\label{sub:baby-set-theory-2}
+
+Show that no two of the three sets $\emptyset$, $\{\emptyset\}$, and
+  $\{\{\emptyset\}\}$ are equal to each other.
+
+\begin{proof}
+
+  By the \nameref{ref:principle-extensionality}, $\emptyset$ is only equal to
+    $\emptyset$.
+  This immediately shows it is not equal to the other two.
+  Now consider object $\emptyset$.
+  This object is a member of $\{\emptyset\}$ but is not a member of
+    $\{\{\emptyset\}\}$.
+  Again, by the \nameref{ref:principle-extensionality}, these two sets must be
+    different.
+
+\end{proof}
+
+\subsection{\partial{Exercise 3}}%
+\label{sub:baby-set-theory-3}
+
+Show that if $B \subseteq C$, then $\mathscr{P} B \subseteq \mathscr{P} C$.
+
+\begin{proof}
+
+  Let $x \in \mathscr{P} B$.
+  By definition of the \nameref{ref:powerset}, $x$ is a subset of $B$.
+  By hypothesis, $B \subseteq C$.
+  Then $x \subseteq C$.
+  Again by definition of the \nameref{ref:powerset}, it follows
+    $x \in \mathscr{P} C$.
+
+\end{proof}
+
+\subsection{\partial{Exercise 4}}%
+\label{sub:baby-set-theory-4}
+
+Assume that $x$ and $y$ are members of a set $B$.
+Show that $\{\{x\}, \{x, y\}\} \in \mathscr{P}\mathscr{P} B.$
+
+\begin{proof}
+
+  Let $x$ and $y$ be members of set $B$.
+  Then $\{x\}$ and $\{x, y\}$ are subsets of $B$.
+  By definition of the \nameref{ref:powerset}, $\{x\}$ and $\{x, y\}$ are
+    members of $\mathscr{P} B$.
+  Then $\{\{x\}, \{x, y\}\}$ is a subset of $\mathscr{P} B$.
+  By definition of the \nameref{ref:powerset}, $\{\{x\}, \{x, y\}\}$ is a member
+    of $\mathscr{P}\mathscr{P} B$.
+
+\end{proof}
+
+\end{document}

Bookshelf/Enderton/Set/Chapter_1.lean

@@ -0,0 +1,13 @@
+import Mathlib.Init.Set
+
+/-! # Enderton.Chapter_1
+
+Introduction
+-/
+
+namespace Enderton.Set.Chapter_1
+
+
+
+
+end Enderton.Set.Chapter_1

Bookshelf/Enderton_Logic.lean

@@ -1 +0,0 @@
-import Bookshelf.Enderton_Logic.Chapter_0

Bookshelf/Enderton_Logic/Chapter_0.lean

@@ -1,10 +0,0 @@
-/-! # Enderton.Chapter_0
-
-Useful Facts About Sets
--/
-
-namespace Enderton.Chapter_0
-
--- TODO
-
-end Enderton.Chapter_0

README.md

@@ -8,6 +8,7 @@ feasible, theorems are also formally proven in [Lean](https://leanprover.github.
 - [ ] Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in Mathematics. Cham: Springer International Publishing, 2015.
 - [ ] Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. 3rd ed. Cambridge, Mass: MIT Press, 2009.
 - [ ] Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001.
+- [ ] Enderton, Herbert B. Elements of Set Theory. New York: Academic Press, 1977.
 - [ ] Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
 - [ ] Gustedt, Jens. Modern C. Shelter Island, NY: Manning Publications Co, 2020.
 - [ ] Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.