Enderton. Well-ordering principle and reorder notes below links.

finite-set-exercises
Joshua Potter 2023-08-10 12:06:20 -06:00
parent 1c988dc9e9
commit ca58d67d8e
1 changed files with 69 additions and 20 deletions

View File

@ -213,6 +213,10 @@
and it is "closed under \nameref{ref:successor}", i.e. and it is "closed under \nameref{ref:successor}", i.e.
$$(\forall a \in A) a^+ \in A.$$ $$(\forall a \in A) a^+ \in A.$$
\lean{Prelude}{Nat}
\lean{Mathlib/Init/Set}{Set.univ}
\begin{note} \begin{note}
Induction is baked into Lean's type system. Induction is baked into Lean's type system.
In particular, the $\emptyset$ and "closed under successor" properties are In particular, the $\emptyset$ and "closed under successor" properties are
@ -220,10 +224,6 @@
respectively. respectively.
\end{note} \end{note}
\lean{Prelude}{Nat}
\lean{Mathlib/Init/Set}{Set.univ}
\section{\defined{Infinity Axiom}}% \section{\defined{Infinity Axiom}}%
\hyperlabel{ref:infinity-axiom} \hyperlabel{ref:infinity-axiom}
@ -266,6 +266,8 @@
\item $R$ is \nameref{ref:trichotomous}. \item $R$ is \nameref{ref:trichotomous}.
\end{enumerate} \end{enumerate}
\lean{Mathlib/Init/Algebra/Classes}{IsStrictTotalOrder}
\begin{note} \begin{note}
This definition does not agree with how Lean defines a linear order. This definition does not agree with how Lean defines a linear order.
@ -284,8 +286,6 @@
\end{enumerate} \end{enumerate}
\end{note} \end{note}
\lean{Mathlib/Init/Algebra/Classes}{IsStrictTotalOrder}
\section{\defined{Multiplication}}% \section{\defined{Multiplication}}%
\hyperlabel{ref:multiplication} \hyperlabel{ref:multiplication}
@ -462,14 +462,14 @@
For any set $a$, its \textbf{successor} is defined by $$a^+ = a \cup \{a\}.$$ For any set $a$, its \textbf{successor} is defined by $$a^+ = a \cup \{a\}.$$
\lean{Prelude}{Nat.succ}
\begin{note} \begin{note}
The corresponding Lean reference refers to the `Nat.succ` constructor. The corresponding Lean definition refers to the `Nat.succ` constructor.
This is not represented internally as a union of sets, but serves the same This is not represented internally as a union of sets, but serves the same
role. role.
\end{note} \end{note}
\lean{Prelude}{Nat.succ}
\section{\defined{Subset Axioms}}% \section{\defined{Subset Axioms}}%
\hyperlabel{ref:subset-axioms} \hyperlabel{ref:subset-axioms}
@ -5763,13 +5763,13 @@
$\langle \omega, \sigma, 0 \rangle$ is a Peano system. $\langle \omega, \sigma, 0 \rangle$ is a Peano system.
\end{theorem} \end{theorem}
\code{Common/Set/Peano}{Peano.instSystemNatUnivSuccOfNatInstOfNatNat}
\begin{note} \begin{note}
This theorem depends on \nameref{sub:theorem-4e} and This theorem depends on \nameref{sub:theorem-4e} and
\nameref{sub:theorem-4f}. \nameref{sub:theorem-4f}.
\end{note} \end{note}
\code{Common/Set/Peano}{Peano.instSystemNatUnivSuccOfNatInstOfNatNat}
\begin{proof} \begin{proof}
Note $\sigma$ is defined as $\sigma = \{\pair{n, n^+} \mid n \in \omega\}$. Note $\sigma$ is defined as $\sigma = \{\pair{n, n^+} \mid n \in \omega\}$.
@ -6590,16 +6590,16 @@
For $m, n \in \omega$, $$m \cdot n = n \cdot m.$$ For $m, n \in \omega$, $$m \cdot n = n \cdot m.$$
\end{theorem} \end{theorem}
\begin{note}
We prove commutativity before associativity, though Enderton orders these
two properties in the opposite direction.
\end{note}
\code{Bookshelf/Enderton/Set/Chapter\_4} \code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_5} {Enderton.Set.Chapter\_4.theorem\_4k\_5}
\lean{Init/Data/Nat/Basic}{Nat.mul\_comm} \lean{Init/Data/Nat/Basic}{Nat.mul\_comm}
\begin{note}
We prove commutativity before associativity, though Enderton orders these
two properties in the opposite direction.
\end{note}
\begin{proof} \begin{proof}
Fix $n \in \omega$ and define Fix $n \in \omega$ and define
@ -6747,12 +6747,12 @@
For any natural numbers $m$ and $n$, $$m \in n \iff m^+ \in n^+.$$ For any natural numbers $m$ and $n$, $$m \in n \iff m^+ \in n^+.$$
\end{lemma} \end{lemma}
\lean{Std/Data/Nat/Lemmas}{Nat.succ\_lt\_succ\_iff}
\begin{note} \begin{note}
Here I referred to Enderton's proof in the forward direction. Here I referred to Enderton's proof in the forward direction.
\end{note} \end{note}
\lean{Std/Data/Nat/Lemmas}{Nat.succ\_lt\_succ\_iff}
\begin{proof} \begin{proof}
Let $m$ and $n$ be \nameref{ref:natural-number}s. Let $m$ and $n$ be \nameref{ref:natural-number}s.
@ -7242,7 +7242,7 @@
\end{proof} \end{proof}
\subsection{\sorry{% \subsection{\pending{%
Well Ordering of \texorpdfstring{$\omega$}{Natural Numbers}}}% Well Ordering of \texorpdfstring{$\omega$}{Natural Numbers}}}%
\hyperlabel{sub:well-ordering-natural-numbers} \hyperlabel{sub:well-ordering-natural-numbers}
@ -7251,8 +7251,57 @@
Then there is some $m \in A$ such that $m \ineq n$ for all $n \in A$. Then there is some $m \in A$ such that $m \ineq n$ for all $n \in A$.
\end{theorem} \end{theorem}
\lean{Mathlib/SetTheory/Ordinal/Basic}{WellOrder}
\begin{note}
This proof was written a few days after reading Enderton's proof as a means
of ensuring I remember the main arguments.
\end{note}
\begin{proof} \begin{proof}
TODO
Let $A$ be a nonempty subset of $\omega$.
For the sake of contradiction, suppose $A$ does not have a least element.
It then suffices to prove that the complement of $A$ equals $\omega$.
If we do so, then $A = \emptyset$, a contradiction.
Define
\begin{equation}
\hyperlabel{sub:well-ordering-natural-numbers-eq1}
S = \{n \in \omega \mid (\forall m \in n) m \not\in A\}.
\end{equation}
We prove $S$ is an \nameref{ref:inductive-set} by showing that (i)
$0 \in S$ and (ii) if $n \in S$, then $n^+ \in S$.
Afterward we show that $\omega - A = \omega$, completing the proof.
\paragraph{(i)}%
\hyperlabel{par:well-ordering-natural-numbers-i}
It vacuously holds that $0 \in S$.
\paragraph{(ii)}%
\hyperlabel{par:well-ordering-natural-numbers-ii}
Suppose $n \in S$.
That is, for all $m \in n$, $m \in \omega - A$.
Let $p$ be an arbitrary element of $A$.
By the \nameref{sub:trichotomy-law-natural-numbers}, only one of the
following holds:
$$p \in n^+, \quad p = n^+, \quad n^+ \in p.$$
It cannot be that $p \in n^+$ since $p \in \omega - A$ by
\eqref{sub:well-ordering-natural-numbers-eq1}.
But then $n^+ = p$ or $n^+ \in p$, implying that $n^+$ is a least element
of $A$.
Since $A$ does not have a least element, it must be that $n^+ \not\in A$.
Hence $n^+ \in S$.
\paragraph{Conclusion}%
By \nameref{par:well-ordering-natural-numbers-i} and
\nameref{par:well-ordering-natural-numbers-ii}, $S$ is an inductive set.
Since $S \subseteq \omega$, \nameref{sub:theorem-4b} implies $S = \omega$.
But this immediately implies $\omega = \omega - A$ meaning $A$ is the
empty set.
\end{proof} \end{proof}
\subsection{\sorry{Corollary 4Q}}% \subsection{\sorry{Corollary 4Q}}%