From ed981c3892712a58f3c6d21b5b724861ac98451d Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 18 May 2023 14:04:20 -0600 Subject: [PATCH] Add start of Enderton's "Elements of Set Theory." --- Bookshelf.lean | 3 +- Bookshelf/Enderton/Logic.lean | 1 + .../Logic.tex} | 4 +- Bookshelf/Enderton/Logic/Chapter_0.lean | 10 + Bookshelf/Enderton/Set.lean | 1 + Bookshelf/Enderton/Set.tex | 190 ++++++++++++++++++ Bookshelf/Enderton/Set/Chapter_1.lean | 13 ++ Bookshelf/Enderton_Logic.lean | 1 - Bookshelf/Enderton_Logic/Chapter_0.lean | 10 - README.md | 1 + 10 files changed, 220 insertions(+), 14 deletions(-) create mode 100644 Bookshelf/Enderton/Logic.lean rename Bookshelf/{Enderton_Logic.tex => Enderton/Logic.tex} (92%) create mode 100644 Bookshelf/Enderton/Logic/Chapter_0.lean create mode 100644 Bookshelf/Enderton/Set.lean create mode 100644 Bookshelf/Enderton/Set.tex create mode 100644 Bookshelf/Enderton/Set/Chapter_1.lean delete mode 100644 Bookshelf/Enderton_Logic.lean delete mode 100644 Bookshelf/Enderton_Logic/Chapter_0.lean diff --git a/Bookshelf.lean b/Bookshelf.lean index 88c1df8..60405a2 100644 --- a/Bookshelf.lean +++ b/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 diff --git a/Bookshelf/Enderton/Logic.lean b/Bookshelf/Enderton/Logic.lean new file mode 100644 index 0000000..dc4ff1f --- /dev/null +++ b/Bookshelf/Enderton/Logic.lean @@ -0,0 +1 @@ +import Bookshelf.Enderton.Logic.Chapter_0 \ No newline at end of file diff --git a/Bookshelf/Enderton_Logic.tex b/Bookshelf/Enderton/Logic.tex similarity index 92% rename from Bookshelf/Enderton_Logic.tex rename to Bookshelf/Enderton/Logic.tex index a0e74f0..d2ba7d2 100644 --- a/Bookshelf/Enderton_Logic.tex +++ b/Bookshelf/Enderton/Logic.tex @@ -1,7 +1,7 @@ \documentclass{report} -\input{../preamble} -\makeleancommands +\input{../../preamble} +\makeleancommands{../..} \begin{document} diff --git a/Bookshelf/Enderton/Logic/Chapter_0.lean b/Bookshelf/Enderton/Logic/Chapter_0.lean new file mode 100644 index 0000000..2280256 --- /dev/null +++ b/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 diff --git a/Bookshelf/Enderton/Set.lean b/Bookshelf/Enderton/Set.lean new file mode 100644 index 0000000..81598b8 --- /dev/null +++ b/Bookshelf/Enderton/Set.lean @@ -0,0 +1 @@ +import Bookshelf.Enderton.Set.Chapter_1 \ No newline at end of file diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex new file mode 100644 index 0000000..49f2d7d --- /dev/null +++ b/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} diff --git a/Bookshelf/Enderton/Set/Chapter_1.lean b/Bookshelf/Enderton/Set/Chapter_1.lean new file mode 100644 index 0000000..9b9b89c --- /dev/null +++ b/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 \ No newline at end of file diff --git a/Bookshelf/Enderton_Logic.lean b/Bookshelf/Enderton_Logic.lean deleted file mode 100644 index a531813..0000000 --- a/Bookshelf/Enderton_Logic.lean +++ /dev/null @@ -1 +0,0 @@ -import Bookshelf.Enderton_Logic.Chapter_0 diff --git a/Bookshelf/Enderton_Logic/Chapter_0.lean b/Bookshelf/Enderton_Logic/Chapter_0.lean deleted file mode 100644 index 079f2a6..0000000 --- a/Bookshelf/Enderton_Logic/Chapter_0.lean +++ /dev/null @@ -1,10 +0,0 @@ -/-! # Enderton.Chapter_0 - -Useful Facts About Sets --/ - -namespace Enderton.Chapter_0 - --- TODO - -end Enderton.Chapter_0 diff --git a/README.md b/README.md index cf107b2..3fea8aa 100644 --- a/README.md +++ b/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.