r
/
bookshelf
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Organize custom proofs over Lean proofs.

finite-set-exercises
Joshua Potter 2023-08-09 15:56:44 -06:00
parent 83699dd58e
commit c4538e3e94
2 changed files with 131 additions and 177 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
Bookshelf/Apostol.tex
View File

@ -1244,7 +1244,7 @@ The union of a finite collection of line segments in a plane.
\section{Exercises 1.11}%
\hyperlabel{sec:exercises-1-11}
\subsection{\pending{Exercise 1.11.4}}%
\subsection{\verified{Exercise 1.11.4}}%
\hyperlabel{sub:exercise-1.11.4}
Prove that the greatest-integer function has the properties indicated:
@ -1254,8 +1254,7 @@ The union of a finite collection of line segments in a plane.
$\floor{x + n} = \floor{x} + n$ for every integer $n$.
% FIXUP: padding
\code{Bookshelf/Apostol/Chapter\_1\_11}
\code*{Bookshelf/Apostol/Chapter\_1\_11}
{Apostol.Chapter\_1\_11.exercise\_4a}
\begin{proof}
@ -1277,8 +1276,7 @@ The union of a finite collection of line segments in a plane.
-\floor{x} - 1 & \text{otherwise}.
\end{cases}$
% FIXUP: padding
\code{Bookshelf/Apostol/Chapter\_1\_11}
\code*{Bookshelf/Apostol/Chapter\_1\_11}
{Apostol.Chapter\_1\_11.exercise\_4b\_1}
\code{Bookshelf/Apostol/Chapter\_1\_11}
@ -1321,8 +1319,7 @@ The union of a finite collection of line segments in a plane.
$\floor{x + y} = \floor{x} + \floor{y}$ or $\floor{x} + \floor{y} + 1$.
% FIXUP: padding
\code{Bookshelf/Apostol/Chapter\_1\_11}
\code*{Bookshelf/Apostol/Chapter\_1\_11}
{Apostol.Chapter\_1\_11.exercise\_4c}
\begin{proof}
@ -1362,26 +1359,24 @@ The union of a finite collection of line segments in a plane.
\end{proof}
\subsubsection{\pending{Exercise 1.11.4d}}%
\subsubsection{\verified{Exercise 1.11.4d}}%
\hyperlabel{ssub:exercise-1.11.4d}
$\floor{2x} = \floor{x} + \floor{x + \frac{1}{2}}.$
% FIXUP: padding
\code{Bookshelf/Apostol/Chapter\_1\_11}
\code*{Bookshelf/Apostol/Chapter\_1\_11}
{Apostol.Chapter\_1\_11.exercise\_4d}
\begin{proof}
This is immediately proven by applying \nameref{sub:hermites-identity}.
\end{proof}
\subsubsection{\pending{Exercise 1.11.4e}}%
\subsubsection{\verified{Exercise 1.11.4e}}%
\hyperlabel{ssub:exercise-1.11.4e}
$\floor{3x} = \floor{x} + \floor{x + \frac{1}{3}} + \floor{x + \frac{2}{3}}.$
% FIXUP: padding
\code{Bookshelf/Apostol/Chapter\_1\_11}
\code*{Bookshelf/Apostol/Chapter\_1\_11}
{Apostol.Chapter\_1\_11.exercise\_4e}
\begin{proof}
@ -1396,8 +1391,7 @@ The union of a finite collection of line segments in a plane.
$\floor{nx}$.
State and prove such a generalization.
% FIXUP: padding
\code{Bookshelf/Apostol/Chapter\_1\_11}
\code*{Bookshelf/Apostol/Chapter\_1\_11}
{Apostol.Chapter\_1\_11.exercise\_5}
\begin{proof}
@ -1626,8 +1620,7 @@ The union of a finite collection of line segments in a plane.
$\sum_{n=1}^{b-1} \floor{na / b} = \sum_{n=1}^{b-1} \floor{a(b - n) / b}$.
Now apply Exercises 4(a) and (b) to the bracket on the right.
% FIXUP: padding
\code{Bookshelf/Apostol/Chapter\_1\_11}
\code*{Bookshelf/Apostol/Chapter\_1\_11}
{Apostol.Chapter\_1\_11.exercise\_7b}
\begin{proof}

327
Bookshelf/Enderton/Set.tex
View File

@ -88,10 +88,10 @@
The \textbf{composition} of sets $F$ and $G$ is
$$F \circ G = \{\pair{u, v} \mid \exists t(uGt \land tFv)\}.$$
\lean{Mathlib/Data/Rel}{Rel.comp}
\code{Bookshelf/Enderton/Set/Relation}{Set.Relation.comp}
\lean{Mathlib/Data/Rel}{Rel.comp}
\section{\defined{Connected}}%
\hyperlabel{ref:connected}
@ -106,10 +106,10 @@
The \textbf{domain} of set $R$, denoted $\dom{R}$, is given by
$$x \in \dom{R} \iff \exists y \pair{x, y} \in R.$$
\lean{Mathlib/Data/Rel}{Rel.dom}
\code{Bookshelf/Enderton/Set/Relation}{Set.Relation.dom}
\lean{Mathlib/Data/Rel}{Rel.dom}
\section{\defined{Empty Set Axiom}}%
\hyperlabel{ref:empty-set-axiom}
@ -202,10 +202,10 @@
& = \{v \mid (\exists u \in A) uFv\}.
\end{align*}
\lean{Mathlib/Data/Rel}{Rel.image}
\code{Bookshelf/Enderton/Set/Relation}{Set.Relation.image}
\lean{Mathlib/Data/Rel}{Rel.image}
\section{\defined{Inductive Set}}%
\hyperlabel{ref:inductive-set}
@ -247,10 +247,10 @@
The \textbf{inverse} of a set $F$ is the set
$$F^{-1} = \{\pair{u, v} \mid vFu\}.$$
\lean{Mathlib/Data/Rel}{Rel.inv}
\code{Bookshelf/Enderton/Set/Relation}{Set.Relation.inv}
\lean{Mathlib/Data/Rel}{Rel.inv}
\section{\defined{Irreflexive}}%
\hyperlabel{ref:irreflexive}
@ -322,9 +322,9 @@
For any sets $u$ and $v$, the \textbf{ordered pair} $\pair{u, v}$ is
the set $\{\{u\}, \{u, v\}\}$.
\lean*{Prelude}{Prod}
\code*{Bookshelf/Enderton/Set/OrderedPair}{OrderedPair}
\code{Bookshelf/Enderton/Set/OrderedPair}{OrderedPair}
\lean{Prelude}{Prod}
\section{\defined{Ordering on \texorpdfstring{$\omega$}{Natural Numbers}}}%
\hyperlabel{ref:ordering-natural-numbers}
@ -432,28 +432,28 @@
The \textbf{range} of set $R$, denoted $\ran{R}$, is given by
$$x \in \ran{R} \iff \exists t \pair{t, x} \in R.$$
\lean{Mathlib/Data/Rel}{Rel.codom}
\code{Bookshelf/Enderton/Set/Relation}{Set.Relation.ran}
\lean{Mathlib/Data/Rel}{Rel.codom}
\section{\defined{Reflexive}}%
\hyperlabel{ref:reflexive}
A binary relation $R$ is \textbf{reflexive} on $A$ if and only if $xRx$ for
all $x \in A$.
\lean*{Mathlib/Init/Algebra/Classes}{IsRefl}
\code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isReflexive}
\code{Bookshelf/Enderton/Set/Relation}{Set.Relation.isReflexive}
\lean{Mathlib/Init/Algebra/Classes}{IsRefl}
\section{\defined{Relation}}%
\hyperlabel{ref:relation}
A \textbf{relation} is a set of \nameref{ref:ordered-pair}s.
\lean*{Mathlib/Data/Rel}{Rel}
\code*{Bookshelf/Enderton/Set/Relation}{Set.Relation}
\code{Bookshelf/Enderton/Set/Relation}{Set.Relation}
\lean{Mathlib/Data/Rel}{Rel}
\section{\defined{Restriction}}%
\hyperlabel{ref:restriction}
@ -507,9 +507,9 @@
A binary relation $R$ is \textbf{transitive} if and only if whenever $xRy$ and
$yRz$, then $xRz$.
\lean*{Mathlib/Init/Algebra/Classes}{IsTrans}
\code*{Bookshelf/Enderton/Set/Relation}{Set.Relation.isTransitive}
\code{Bookshelf/Enderton/Set/Relation}{Set.Relation.isTransitive}
\lean{Mathlib/Init/Algebra/Classes}{IsTrans}
\section{\defined{Transitive Set}}%
\hyperlabel{ref:transitive-set}
@ -887,29 +887,24 @@
\hyperlabel{sub:commutative-laws}
For any sets $A$ and $B$,
\begin{align*}
A \cup B = B \cup A \\
A \cap B = B \cap A
\end{align*}
\lean{Mathlib/Data/Set/Basic}{Set.union\_comm}
\begin{enumerate}[(i)]
\item $A \cup B = B \cup A$
\item $A \cap B = B \cap A$
\end{enumerate}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.commutative\_law\_i}
\lean{Mathlib/Data/Set/Basic}{Set.inter\_comm}
\lean{Mathlib/Data/Set/Basic}{Set.union\_comm}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.commutative\_law\_ii}
\lean{Mathlib/Data/Set/Basic}{Set.inter\_comm}
\begin{proof}
Let $A$ and $B$ be sets.
We prove that
\begin{enumerate}[(i)]
\item $A \cup B = B \cup A$
\item $A \cap B = B \cap A$.
\end{enumerate}
\paragraph{(i)}%
@ -937,30 +932,25 @@
\hyperlabel{sub:associative-laws}
For any sets $A$, $B$ and $C$,
\begin{align*}
A \cup (B \cup C) & = (A \cup B) \cup C \\
A \cap (B \cap C) & = (A \cap B) \cap C
\end{align*}
\lean{Mathlib/Data/Set/Basic}{Set.union\_assoc}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.associative\_law\_i}
\lean{Mathlib/Data/Set/Basic}{Set.inter\_assoc}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.associative\_law\_ii}
\begin{proof}
Let $A$, $B$, and $C$ be sets.
We prove that
\begin{enumerate}[(i)]
\item $A \cup (B \cup C) = (A \cup B) \cup C$
\item $A \cap (B \cap C) = (A \cap B) \cap C$
\end{enumerate}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.associative\_law\_i}
\lean{Mathlib/Data/Set/Basic}{Set.union\_assoc}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.associative\_law\_ii}
\lean{Mathlib/Data/Set/Basic}{Set.inter\_assoc}
\begin{proof}
Let $A$, $B$, and $C$ be sets.
\paragraph{(i)}%
By the definition of the union of sets,
@ -991,30 +981,25 @@
\hyperlabel{sub:distributive-laws}
For any sets $A$, $B$, and $C$,
\begin{align*}
A \cap (B \cup C) & = (A \cap B) \cup (A \cap C) \\
A \cup (B \cap C) & = (A \cup B) \cap (A \cup C)
\end{align*}
\lean{Mathlib/Data/Set/Basic}{Set.inter\_distrib\_left}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.distributive\_law\_i}
\lean{Mathlib/Data/Set/Basic}{Set.union\_distrib\_left}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.distributive\_law\_ii}
\begin{proof}
Let $A$, $B$, and $C$ be sets.
We prove that
\begin{enumerate}[(i)]
\item $A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$
\item $A \cup (B \cap C) = (A \cup B) \cap (A \cup C)$
\end{enumerate}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.distributive\_law\_i}
\lean{Mathlib/Data/Set/Basic}{Set.inter\_distrib\_left}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.distributive\_law\_ii}
\lean{Mathlib/Data/Set/Basic}{Set.union\_distrib\_left}
\begin{proof}
Let $A$, $B$, and $C$ be sets.
\paragraph{(i)}%
By the definition of the union and intersection of sets,
@ -1052,16 +1037,16 @@
\item $C - (A \cap B) = (C - A) \cup (C - B)$
\end{enumerate}
\lean{Mathlib/Data/Set/Basic}{Set.diff\_inter\_diff}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.de\_morgans\_law\_i}
\lean{Mathlib/Data/Set/Basic}{Set.diff\_inter}
\lean{Mathlib/Data/Set/Basic}{Set.diff\_inter\_diff}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.de\_morgans\_law\_ii}
\lean{Mathlib/Data/Set/Basic}{Set.diff\_inter}
\begin{proof}
Let $A$, $B$, and $C$ be sets.
@ -1109,21 +1094,21 @@
\item $A \cap (C - A) = \emptyset$
\end{enumerate}
\lean{Mathlib/Data/Set/Basic}{Set.union\_empty}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.emptyset\_identity\_i}
\lean{Mathlib/Data/Set/Basic}{Set.inter\_empty}
\lean{Mathlib/Data/Set/Basic}{Set.union\_empty}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.emptyset\_identity\_ii}
\lean{Mathlib/Data/Set/Basic}{Set.inter\_diff\_self}
\lean{Mathlib/Data/Set/Basic}{Set.inter\_empty}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.emptyset\_identity\_iii}
\lean{Mathlib/Data/Set/Basic}{Set.inter\_diff\_self}
\begin{proof}
Let $A$ be an arbitrary set.
@ -1169,40 +1154,34 @@
\hyperlabel{sub:monotonicity}
For any sets $A$, $B$, and $C$,
\begin{align*}
A \subseteq B & \Rightarrow A \cup C \subseteq B \cup C \\
A \subseteq B & \Rightarrow A \cap C \subseteq B \cap C \\
A \subseteq B & \Rightarrow \bigcup A \subseteq \bigcup B
\end{align*}
\lean{Mathlib/Data/Set/Basic}
{Set.union\_subset\_union\_left}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.monotonicity\_i}
\lean{Mathlib/Data/Set/Basic}
{Set.inter\_subset\_inter\_left}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.monotonicity\_ii}
\lean{Mathlib/Data/Set/Lattice}
{Set.sUnion\_mono}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.monotonicity\_iii}
\begin{proof}
Let $A$, $B$, and $C$ be arbitrary sets.
We prove that
\begin{enumerate}[(i)]
\item $A \subseteq B \Rightarrow A \cup C \subseteq B \cup C$
\item $A \subseteq B \Rightarrow A \cap C \subseteq B \cap C$
\item $A \subseteq B \Rightarrow \bigcup A \subseteq \bigcup B$
\end{enumerate}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.monotonicity\_i}
\lean{Mathlib/Data/Set/Basic}
{Set.union\_subset\_union\_left}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.monotonicity\_ii}
\lean{Mathlib/Data/Set/Basic}
{Set.inter\_subset\_inter\_left}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.monotonicity\_iii}
\lean{Mathlib/Data/Set/Lattice}
{Set.sUnion\_mono}
\begin{proof}
Let $A$, $B$, and $C$ be arbitrary sets.
\paragraph{(i)}%
Suppose $A \subseteq B$.
@ -1252,32 +1231,27 @@
\hyperlabel{sub:anti-monotonicity}
For any sets $A$, $B$, and $C$,
\begin{align*}
A \subseteq B & \Rightarrow C - B \subseteq C - A \\
\emptyset \neq A \subseteq B & \Rightarrow \bigcap B \subseteq \bigcap A.
\end{align*}
\begin{enumerate}[(i)]
\item $A \subseteq B \Rightarrow C - B \subseteq C - A$
\item $\emptyset \neq A \subseteq B \Rightarrow
\bigcap B \subseteq \bigcap A$.
\end{enumerate}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.anti\_monotonicity\_i}
\lean{Mathlib/Data/Set/Basic}
{Set.diff\_subset\_diff\_right}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.anti\_monotonicity\_i}
{Enderton.Set.Chapter\_2.anti\_monotonicity\_ii}
\lean{Mathlib/Data/Set/Lattice}
{Set.sInter\_subset\_sInter}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.anti\_monotonicity\_ii}
\begin{proof}
Let $A$, $B$, and $C$ be arbitrary sets.
We prove that
\begin{enumerate}[(i)]
\item $A \subseteq B \Rightarrow C - B \subseteq C - A$
\item $\emptyset \neq A \subseteq B \Rightarrow
\bigcap B \subseteq \bigcap A$
\end{enumerate}
\paragraph{(i)}%
@ -1308,25 +1282,17 @@
\hyperlabel{sub:general-distributive-laws}
For any sets $A$ and $\mathscr{B}$,
\begin{align*}
A \cup \bigcap \mathscr{B} & =
\begin{enumerate}[(i)]
\item $A \cup \bigcap \mathscr{B} =
\bigcap\; \{ A \cup X \mid X \in \mathscr{B} \}
\quad\text{for}\quad \mathscr{B} \neq \emptyset \\
A \cap \bigcup \mathscr{B} & =
\bigcup\; \{ A \cap X \mid X \in \mathscr{B} \}
\end{align*}
\quad\text{for}\quad \mathscr{B} \neq \emptyset$
\item $A \cap \bigcup \mathscr{B} =
\bigcup\; \{ A \cap X \mid X \in \mathscr{B} \}$
\end{enumerate}
\begin{proof}
Let $A$ and $\mathscr{B}$ be sets.
We prove that
\begin{enumerate}[(i)]
\item For $\mathscr{B} \neq \emptyset$,
$A \cup \bigcap \mathscr{B} =
\bigcap\; \{ A \cup X \mid X \in \mathscr{B} \}$.
\item $A \cap \bigcup \mathscr{B} =
\bigcup\; \{ A \cap X \mid X \in \mathscr{B} \}$
\end{enumerate}
\paragraph{(i)}%
@ -1368,15 +1334,6 @@
\hyperlabel{sub:general-de-morgans-laws}
For any set $C$ and $\mathscr{A} \neq \emptyset$,
\begin{align*}
C - \bigcup \mathscr{A} & = \bigcap\; \{ C - X \mid X \in \mathscr{A} \} \\
C - \bigcap \mathscr{A} & = \bigcup\; \{ C - X \mid X \in \mathscr{A} \}
\end{align*}
\begin{proof}
Let $C$ and $\mathscr{A}$ be sets such that $\mathscr{A} \neq \emptyset$.
We prove that
\begin{enumerate}[(i)]
\item $C - \bigcup \mathscr{A} =
\bigcap\; \{ C - X \mid X \in \mathscr{A} \}$
@ -1384,6 +1341,10 @@
\bigcup\; \{ C - X \mid X \in \mathscr{A} \}$
\end{enumerate}
\begin{proof}
Let $C$ and $\mathscr{A}$ be sets such that $\mathscr{A} \neq \emptyset$.
\paragraph{(i)}%
By definition of the relative complement, union, and intersection of sets,
@ -1431,12 +1392,12 @@
Let $A$, $B$, and $C$ be sets.
Then $A \cap (B - C) = (A \cap B) - C$.
\lean*{Mathlib/Data/Set/Basic}
{Set.inter\_diff\_assoc}
\code{Bookshelf/Enderton/Set/Chapter\_2}
\code*{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.inter\_diff\_assoc}
\lean{Mathlib/Data/Set/Basic}
{Set.inter\_diff\_assoc}
\begin{proof}
Let $A$, $B$, and $C$ be sets.
By definition of the intersection and relative complement of sets,
@ -1953,12 +1914,12 @@
Show that $A \cap (B + C) = (A \cap B) + (A \cap C)$.
\lean*{Mathlib/Data/Set/Basic}
{Set.inter\_symmDiff\_distrib\_left}
\code{Bookshelf/Enderton/Set/Chapter\_2}
\code*{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.exercise\_2\_15a}
\lean{Mathlib/Data/Set/Basic}
{Set.inter\_symmDiff\_distrib\_left}
\begin{proof}
By definition of the intersection, \nameref{ref:symmetric-difference}, and
relative complement of sets,
@ -1992,11 +1953,11 @@
Show that $A + (B + C) = (A + B) + C$.
\lean*{Mathlib/Order/SymmDiff}{symmDiff\_assoc}
\code{Bookshelf/Enderton/Set/Chapter\_2}
\code*{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.exercise\_2\_15b}
\lean{Mathlib/Order/SymmDiff}{symmDiff\_assoc}
\begin{proof}
Let $A$, $B$, and $C$ be sets.
We prove that
@ -6094,13 +6055,13 @@
\end{align}
\end{theorem}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4i}
\lean{Init/Data/Nat/Basic}{Nat.add\_zero}
\lean{Init/Prelude}{Nat.add}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4i}
\begin{proof}
\paragraph{\eqref{sub:theorem-4i-eq1}}%
@ -6129,13 +6090,13 @@
\end{align}
\end{theorem}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4j}
\lean{Init/Data/Nat/Basic}{Nat.mul\_zero}
\lean{Init/Prelude}{Nat.mul}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4j}
\begin{proof}
\paragraph{\eqref{sub:theorem-4j-eq1}}%
@ -6159,11 +6120,11 @@
In other words, $$0 + n = n.$$
\end{lemma}
\lean{Init/Data/Nat/Basic}{Nat.zero\_add}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.left\_additive\_identity}
\lean{Init/Data/Nat/Basic}{Nat.zero\_add}
\begin{proof}
Let $S = \{n \in \omega \mid 0 + n = n\}$.
@ -6203,11 +6164,11 @@
In other words, $$m^+ + n = m + n^+.$$
\end{lemma}
\lean{Std/Data/Nat/Lemmas}{Nat.succ\_add\_eq\_succ\_add}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.lemma\_2}
\lean{Std/Data/Nat/Lemmas}{Nat.succ\_add\_eq\_succ\_add}
\begin{proof}
Let $m \in \omega$ and define
@ -6247,11 +6208,11 @@
For $m, n, p \in \omega$, $$m + (n + p) = (m + n) + p.$$
\end{theorem}
\lean{Init/Data/Nat/Basic}{Nat.add\_assoc}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_1}
\lean{Init/Data/Nat/Basic}{Nat.add\_assoc}
\begin{proof}
Fix $n, p \in \omega$ and define
@ -6304,11 +6265,11 @@
For $m, n \in \omega$, $$m + n = n + m.$$
\end{theorem}
\lean{Init/Data/Nat/Basic}{Nat.add\_comm}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_2}
\lean{Init/Data/Nat/Basic}{Nat.add\_comm}
\begin{proof}
Fix $n \in \omega$ and define
@ -6357,11 +6318,11 @@
In other words, $$0 \cdot n = 0.$$
\end{lemma}
\lean{Init/Data/Nat/Basic}{Nat.zero\_mul}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.zero\_multiplicand}
\lean{Init/Data/Nat/Basic}{Nat.zero\_mul}
\begin{proof}
Define
@ -6409,11 +6370,11 @@
In other words, $$m^+ \cdot n = m \cdot n + n.$$
\end{lemma}
\lean{Init/Data/Nat/Basic}{Nat.succ\_mul}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.succ\_distrib}
\lean{Init/Data/Nat/Basic}{Nat.succ\_mul}
\begin{proof}
Let $m \in \omega$ and define
@ -6466,11 +6427,11 @@
For $m, n, p \in \omega$, $$m \cdot (n + p) = m \cdot n + m \cdot p.$$
\end{theorem}
\lean{Init/Data/Nat/Basic}{Nat.left\_distrib}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_3}
\lean{Init/Data/Nat/Basic}{Nat.left\_distrib}
\begin{proof}
Fix $n, p \in \omega$ and define
@ -6529,11 +6490,11 @@
In other words, $$m + 1 = m^+.$$
\end{lemma}
\lean{Std/Data/Nat/Lemmas}{Nat.succ\_eq\_one\_add}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.succ\_identity}
\lean{Std/Data/Nat/Lemmas}{Nat.succ\_eq\_one\_add}
\begin{proof}
Let
@ -6583,11 +6544,11 @@
In other words, $$m \cdot 1 = m.$$
\end{lemma}
\lean{Init/Data/Nat/Basic}{Nat.mul\_one}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.right\_mul\_id}
\lean{Init/Data/Nat/Basic}{Nat.mul\_one}
\begin{proof}
Let
@ -6640,11 +6601,11 @@
two properties in the opposite direction.
\end{note}
\lean{Init/Data/Nat/Basic}{Nat.mul\_comm}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_5}
\lean{Init/Data/Nat/Basic}{Nat.mul\_comm}
\begin{proof}
Fix $n \in \omega$ and define
@ -6696,11 +6657,11 @@
For $m, n, p \in \omega$, $$m \cdot (n \cdot p) = (m \cdot n) \cdot p.$$
\end{theorem}
\lean{Init/Data/Nat/Basic}{Nat.mul\_assoc}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_4}
\lean{Init/Data/Nat/Basic}{Nat.mul\_assoc}
\begin{proof}
Fix $m, n \in \omega$ and define
@ -6858,11 +6819,11 @@
No natural number is a member of itself.
\end{lemma}
\lean{Init/Prelude}{Nat.lt\_irrefl}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4l\_b}
\lean{Init/Prelude}{Nat.lt\_irrefl}
\begin{proof}
Define
@ -7255,10 +7216,10 @@
\end{align}
\end{corollary}
\lean{Init/Data/Nat/Basic}{Nat.add\_right\_cancel}
\code{Common/Nat/Basic}{Nat.mul\_right\_cancel}
\lean{Init/Data/Nat/Basic}{Nat.add\_right\_cancel}
\begin{proof}
\paragraph{\eqref{sub:corollary-4p-eq1}}%