diff --git a/Bookshelf/Apostol.tex b/Bookshelf/Apostol.tex index 2596d9c..45fbc10 100644 --- a/Bookshelf/Apostol.tex +++ b/Bookshelf/Apostol.tex @@ -187,7 +187,7 @@ That is to say, for each $k = 1, 2, \ldots, n$, there is a real number $s_k$ \begin{note} At each of the endpoints $x_{k-1}$ and $x_k$ the function must have some - well-defined value, but this need not be the same as $s_k$. + well-defined value, but this need not be the same as $s_k$. \end{note} \begin{definition} @@ -1614,8 +1614,8 @@ If $a$ and $b$ are positive integers with no common factor, we have the formula When $b = 1$, the sum on the left is understood to be $0$. \begin{note} - When $b = 1$, the proofs of (a) and (b) are trivial. We continue under the - assumption $b > 1$. + When $b = 1$, the proofs of (a) and (b) are trivial. + We continue under the assumption $b > 1$. \end{note} \subsubsection{\pending{Exercise 1.11.7a}}% diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 3375056..cb08678 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -83,8 +83,12 @@ The \textbf{composition} of sets $F$ and $G$ is \begin{definition} + \statementpadding + \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.comp} + \lean*{Mathlib/Data/Rel}{Rel.comp} + \end{definition} \section{\defined{Connected}}% @@ -106,8 +110,12 @@ The \textbf{domain} of set $R$, denoted $\dom{R}$, is given by \begin{definition} + \statementpadding + \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.dom} + \lean*{Mathlib/Data/Rel}{Rel.dom} + \end{definition} \section{\defined{Empty Set Axiom}}% @@ -215,10 +223,60 @@ The \textbf{image of $A$ under $F$} is the set \begin{definition} + \statementpadding + \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.image} + \lean*{Mathlib/Data/Rel}{Rel.image} + \end{definition} +\section{\defined{Inductive Set}}% +\hyperlabel{ref:inductive-set} + +A set $A$ is said to be \textit{inductive} if and only if $\emptyset \in A$ and + it is "closed under \nameref{ref:successor}", i.e. + $$(\forall a \in A) a^+ \in A.$$ + +\begin{note} + Induction is baked into Lean's type system. + In particular, the $\emptyset$ and "closed under successor" properties are + analagous to base and recursive constructors of an inductive data type + respectively. +\end{note} + +\begin{definition} + + \statementpadding + + \lean*{Prelude}{Nat} + + \lean*{Mathlib/Init/Set}{Set.univ} + +\end{definition} + +\section{\defined{Infinity Axiom}}% +\hyperlabel{ref:infinity-axiom} + +There exists an \nameref{ref:inductive-set}: + $$(\exists A)\left[ \emptyset \in A \land (\forall a \in A) a^+ \in A \right].$$ + +\begin{note} + Since the definition of natural numbers in Lean satisfies the properties + required by this axiom, there is no need to explicitly state the axiom + separately in Lean. +\end{note} + +\begin{axiom} + + \statementpadding + + \lean*{Prelude}{Nat} + + \lean*{Mathlib/Init/Set}{Set.univ} + +\end{axiom} + \section{\defined{Inverse}}% \hyperlabel{ref:inverse} @@ -227,8 +285,12 @@ The \textbf{inverse} of a set $F$ is the set \begin{definition} + \statementpadding + \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.inv} + \lean{Mathlib/Data/Rel}{Rel.inv} + \end{definition} \section{\defined{Irreflexive}}% @@ -260,8 +322,9 @@ A \textbf{linear ordering} on $A$ (also called a \textbf{total ordering} on $A$) \vspace{6pt} Trichotomy is equivalent to asymmetry and connectivity and asymmetry is - equivalent to antisymmetry and irreflexivity. Thus a linear order, as defined - by Enderton, is a binary relation with the following four properties: + equivalent to antisymmetry and irreflexivity. + Thus a linear order, as defined by Enderton, is a binary relation with the + following four properties: \vspace{6pt} \begin{enumerate}[(i)] @@ -278,6 +341,19 @@ A \textbf{linear ordering} on $A$ (also called a \textbf{total ordering} on $A$) \end{definition} +\section{\defined{Natural Number}}% +\hyperlabel{ref:natural-number} + +A \textbf{natural number} is a set that belongs to every inductive set. +The set of all natural numbers exists by virtue of \nameref{sub:theorem-4a}. +This set is denoted as $\omega$. + +\begin{definition} + + \lean*{Prelude}{Nat} + +\end{definition} + \section{\defined{Ordered Pair}}% \hyperlabel{ref:ordered-pair} @@ -286,8 +362,12 @@ For any sets $u$ and $v$, the \textbf{ordered pair} $\pair{u, v}$ is \begin{definition} + \statementpadding + \lean*{Bookshelf/Enderton/Set/OrderedPair}{OrderedPair} + \lean*{Prelude}{Prod} + \end{definition} \section{\defined{Pair Set}}% @@ -385,8 +465,12 @@ The \textbf{range} of set $R$, denoted $\ran{R}$, is given by \begin{definition} + \statementpadding + \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.ran} + \lean*{Mathlib/Data/Rel}{Rel.codom} + \end{definition} \section{\defined{Reflexive}}% @@ -397,8 +481,12 @@ A binary relation $R$ is \textbf{reflexive} on $A$ if and only if $xRx$ for all \begin{definition} + \statementpadding + \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isReflexive} + \lean*{Mathlib/Init/Algebra/Classes}{IsRefl} + \end{definition} \section{\defined{Relation}}% @@ -408,8 +496,12 @@ A \textbf{relation} is a set of \nameref{ref:ordered-pair}s. \begin{definition} + \statementpadding + \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation} + \lean*{Mathlib/Data/Rel}{Rel} + \end{definition} \section{\defined{Restriction}}% @@ -424,6 +516,23 @@ The \textbf{restriction} of a set $F$ to set $A$ is the set \end{definition} +\section{\defined{Successor}}% +\label{ref:successor} + +For any set $a$, its \textbf{successor} is defined by $$a^+ = a \cup \{a\}.$$ + +\begin{note} + The corresponding Lean reference refers to the `Nat.succ` constructor. + This is not represented internally as a union of sets, but serves the same + role. +\end{note} + +\begin{definition} + + \lean*{Prelude}{Nat.succ} + +\end{definition} + \section{\defined{Subset Axioms}}% \hyperlabel{ref:subset-axioms} @@ -469,8 +578,12 @@ A binary relation $R$ is \textbf{transitive} if and only if whenever $xRy$ and \begin{definition} + \statementpadding + \lean*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isTransitive} + \lean*{Mathlib/Init/Algebra/Classes}{IsTrans} + \end{definition} \section{\defined{Trichotomous}}% @@ -2690,8 +2803,8 @@ If not, then under what conditions does equality hold? \lean*{Mathlib/SetTheory/ZFC/Basic}{Set.prod} \begin{note} - The above Lean proof is a definition (i.e. an axiom). It does not prove - such a set's existence from first principles. + The above Lean proof is a definition (i.e. an axiom). + It does not prove such a set's existence from first principles. \end{note} Define $C = A \cup B$. @@ -5806,4 +5919,123 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} +\chapter{Natural Numbers}% +\hyperlabel{chap:natural-numbers} + +\section{Inductive Sets}% +\hyperlabel{sec:inductive-sets} + +\subsection{\unverified{Theorem 4A}}% +\hyperlabel{sub:theorem-4a} + +\begin{theorem}[4A] + + There is a set whose members are exactly the natural numbers. + +\end{theorem} + +\begin{proof} + + By the \nameref{ref:infinity-axiom}, there exists an + \nameref{ref:inductive-set} $A$. + By the \nameref{ref:subset-axioms}, there exists a set $B$ such that + $$x \in B \iff x \in A \land \left[\forall C, + (\emptyset \in C \land + (\forall c \in C) c^+ \in C) \Rightarrow x \in C\right].$$ + In other words, $x \in B$ if and only if $x \in A$ and $x$ is a natural + number. + Thus $B$ is the set whose members are exactly the natural numbers. + +\end{proof} + +\subsection{\unverified{Theorem 4B}}% +\hyperlabel{sub:theorem-4b} + +\begin{theorem}[4B] + + $\omega$ is inductive, and is a subset of every other inductive set. + +\end{theorem} + +\begin{proof} + + $\omega$ denotes the set of \nameref{ref:natural-number}s. + We show $\omega$ is an \nameref{ref:inductive-set} by proving (i) + $\emptyset \in \omega$ and (ii) $\omega$ is closed under + \nameref{ref:successor}. + + \paragraph{(i)}% + \hyperlabel{par:theorem-4b-i} + + By definition, $\emptyset$ is a member of every inductive set. + Thus $\emptyset$ is a natural number, i.e. a member of $\omega$. + + \paragraph{(ii)}% + \hyperlabel{par:theorem-4b-ii} + + Let $n \in \omega$. + That is, let $n$ be a natural number. + By definition, $n$ is a member of every inductive set. + By definition of an inductive set, $n^+$ is then a member of every inductive + set as well. + Thus $n^+$ is a natural number, i.e. $n^+ \in \omega$. + + \paragraph{Conclusion}% + + By \nameref{par:theorem-4b-i} and \nameref{par:theorem-4b-ii}, it follows + $\omega$ is inductive. + It follows immediately from the definition of a natural number that $\omega$ + is a subset of every other inductive set. + +\end{proof} + +\subsection{\verified{Theorem 4C}}% +\hyperlabel{sub:theorem-4c} + +\begin{theorem}[4C] + + Every natural number except $0$ is the successor of some natural number. + +\end{theorem} + +\begin{proof} + + \lean{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4c} + + Let $T = \{n \mid n = 0 \lor (\exists m) n = m^+\}$. + It trivially follows that $\emptyset \in T$. + Let $x \in T$. + Then $x^+ \in T$ since $(\exists m) x^+ = m^+$, namely $m = x$. + Therefore $T$ is inductive. + By \nameref{sub:theorem-4b}, $\omega$ is a subset of $T$. + Thus every natural number satisfies the condition written in $T$'s definition. + In other words, every natural number except $0$ is the successor of some + natural number. + +\end{proof} + +\section{Exercises 4}% +\hyperlabel{sec:exercises-4} + +\subsection{\verified{Exercise 4.1}}% +\label{sub:exercise-4.1} + +Show that $1 \neq 3$ i.e., that $\emptyset^+ \neq \emptyset^{+++}$. + +\begin{proof} + + \lean{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.exercise\_4\_1} + + By definition, + \begin{align*} + 1 & = \{\emptyset\} \\ + 3 & = \{\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}\}. + \end{align*} + By the \nameref{ref:extensionality-axiom}, these two sets are trivially not + equal to one another. + +\end{proof} + \end{document} diff --git a/Bookshelf/Enderton/Set/Chapter_4.lean b/Bookshelf/Enderton/Set/Chapter_4.lean new file mode 100644 index 0000000..7da5f45 --- /dev/null +++ b/Bookshelf/Enderton/Set/Chapter_4.lean @@ -0,0 +1,27 @@ +import Mathlib.Data.Set.Basic + +/-! # Enderton.Set.Chapter_4 + +Natural Numbers +-/ + +namespace Enderton.Set.Chapter_4 + +/-- #### Theorem 4C + +Every natural number except `0` is the successor of some natural number. +-/ +theorem theorem_4c (n : ℕ) + : n = 0 ∨ (∃ m : ℕ, n = m.succ) := by + match n with + | 0 => simp + | m + 1 => simp + +/-- #### Exercise 4.1 + +Show that `1 ≠ 3` i.e., that `∅⁺ ≠ ∅⁺⁺⁺`. +-/ +theorem exercise_4_1 : 1 ≠ 3 := by + simp + +end Enderton.Set.Chapter_4 \ No newline at end of file