From ec53cdd710a78a25589f7ab97071779ad94619cc Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 8 Aug 2023 17:30:29 -0600 Subject: [PATCH] Update proofs to pending if there is no custom proof set. --- Bookshelf/Enderton/Set.tex | 65 +++++++++++++++++++------------------- 1 file changed, 33 insertions(+), 32 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 912efc8..cd36fcc 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -1114,7 +1114,7 @@ List all the members of $V_4$. \section{Algebra of Sets}% \hyperlabel{sec:algebra-sets} -\subsection{\verified{Commutative Laws}}% +\subsection{\pending{Commutative Laws}}% \hyperlabel{sub:commutative-laws} For any sets $A$ and $B$, @@ -1160,7 +1160,7 @@ For any sets $A$ and $B$, \end{proof} -\subsection{\verified{Associative Laws}}% +\subsection{\pending{Associative Laws}}% \hyperlabel{sub:associative-laws} For any sets $A$, $B$ and $C$, @@ -1217,7 +1217,7 @@ For any sets $A$, $B$ and $C$, \end{proof} -\subsection{\verified{Distributive Laws}}% +\subsection{\pending{Distributive Laws}}% \hyperlabel{sub:distributive-laws} For any sets $A$, $B$, and $C$, @@ -1273,7 +1273,7 @@ For any sets $A$, $B$, and $C$, \end{proof} -\subsection{\verified{De Morgan's Laws}}% +\subsection{\pending{De Morgan's Laws}}% \hyperlabel{sub:de-morgans-laws} For any sets $A$, $B$, and $C$, @@ -1331,7 +1331,7 @@ For any sets $A$, $B$, and $C$, \end{proof} -\subsection{\verified{% +\subsection{\pending{% Identities Involving \texorpdfstring{$\emptyset$}{the Empty Set}}}% \hyperlabel{sub:identitives-involving-empty-set} @@ -1401,7 +1401,7 @@ For any set $A$, \end{proof} -\subsection{\verified{Monotonicity}}% +\subsection{\pending{Monotonicity}}% \hyperlabel{sub:monotonicity} For any sets $A$, $B$, and $C$, @@ -1474,7 +1474,7 @@ For any sets $A$, $B$, and $C$, \end{proof} -\subsection{\verified{Anti-monotonicity}}% +\subsection{\pending{Anti-monotonicity}}% \hyperlabel{sub:anti-monotonicity} For any sets $A$, $B$, and $C$, @@ -1644,7 +1644,7 @@ For any set $C$ and $\mathscr{A} \neq \emptyset$, \end{proof} -\subsection{\verified{% +\subsection{\pending{% \texorpdfstring{$\cap$/$-$}{Intersection/Difference} Associativity}}% \hyperlabel{sub:intersection-difference-associativity} @@ -2187,7 +2187,7 @@ Show by example that for some sets $A$, $B$, and $C$, the set $A - (B - C)$ is \end{proof} -\subsection{\verified{Exercise 2.15a}}% +\subsection{\pending{Exercise 2.15a}}% \hyperlabel{sub:exercise-2.15a} Show that $A \cap (B + C) = (A \cap B) + (A \cap C)$. @@ -2224,7 +2224,7 @@ Show that $A \cap (B + C) = (A \cap B) + (A \cap C)$. \end{proof} -\subsection{\verified{Exercise 2.15b}}% +\subsection{\pending{Exercise 2.15b}}% \hyperlabel{sub:exercise-2.15b} Show that $A + (B + C) = (A + B) + C$. @@ -2914,7 +2914,7 @@ If not, then under what conditions does equality hold? \end{proof} -\subsection{\verified{Corollary 3C}}% +\subsection{\pending{Corollary 3C}}% \hyperlabel{sub:corollary-3c} \begin{theorem}[3C] @@ -3730,7 +3730,8 @@ If not, then under what conditions does equality hold? \begin{proof} - \lean{Bookshelf/Enderton/Set/Relation}{Set.Relation.modEquiv\_partition} + \lean{Bookshelf/Enderton/Set/Relation} + {Set.Relation.modEquiv\_partition} Let $\Pi = \{[x]_R \mid x \in A\}$. We show that (i) there are no empty sets in $\Pi$, (ii) no two different sets @@ -4345,7 +4346,7 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive \end{answer} -\subsection{\verified{Exercise 3.11}}% +\subsection{\pending{Exercise 3.11}}% \hyperlabel{sub:exercise-3.11} Prove the following version (for functions) of the extensionality principle: @@ -6527,7 +6528,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \section{Arithmetic}% \hyperlabel{sec:arithmetic} -\subsection{\verified{Theorem 4I}} +\subsection{\pending{Theorem 4I}} \hyperlabel{sub:theorem-4i} \begin{theorem}[4I] @@ -6563,7 +6564,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Theorem 4J}} +\subsection{\pending{Theorem 4J}} \hyperlabel{sub:theorem-4j} \begin{theorem}[4J] @@ -6597,7 +6598,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Left Additive Identity}}% +\subsection{\pending{Left Additive Identity}}% \hyperlabel{sub:left-additive-identity} \begin{lemma} @@ -6639,7 +6640,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Lemma 3}}% +\subsection{\pending{Lemma 3}}% \hyperlabel{sub:lemma-3} \hyperlabel{sub:succ-add-eq-add-succ} @@ -6683,7 +6684,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Theorem 4K-1}}% +\subsection{\pending{Theorem 4K-1}}% \label{sub:theorem-4k-1} \begin{theorem}[4K-1] @@ -6739,7 +6740,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Theorem 4K-2}}% +\subsection{\pending{Theorem 4K-2}}% \label{sub:theorem-4k-2} \begin{theorem}[4K-2] @@ -6791,7 +6792,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Zero Multiplicand}}% +\subsection{\pending{Zero Multiplicand}}% \hyperlabel{sub:zero-multiplicand} \begin{lemma} @@ -6841,7 +6842,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Successor Distribution}}% +\subsection{\pending{Successor Distribution}}% \hyperlabel{sub:successor-distribution} \begin{lemma} @@ -6897,7 +6898,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Theorem 4K-3}} +\subsection{\pending{Theorem 4K-3}} \hyperlabel{sub:theorem-4k-3} \begin{theorem}[4K-3] @@ -6958,7 +6959,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Successor Identity}}% +\subsection{\pending{Successor Identity}}% \hyperlabel{sub:successor-identity} \begin{lemma} @@ -7011,7 +7012,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Right Multiplicative Identity}}% +\subsection{\pending{Right Multiplicative Identity}}% \hyperlabel{sub:right-multiplicative-identity} \begin{lemma} @@ -7062,7 +7063,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Theorem 4K-5}} +\subsection{\pending{Theorem 4K-5}} \hyperlabel{sub:theorem-4k-5} \begin{theorem}[4K-5] @@ -7122,7 +7123,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Theorem 4K-4}}% +\subsection{\pending{Theorem 4K-4}}% \hyperlabel{sub:theorem-4k-4} \begin{theorem}[4K-4] @@ -7180,7 +7181,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \section{Ordering on \texorpdfstring{$\omega$}{Natural Numbers}}% \hyperlabel{sec:ordering-natural-numbers} -\subsection{\verified{Ordering on Successor}}% +\subsection{\pending{Ordering on Successor}}% \hyperlabel{sub:ordering-successor} \begin{lemma} @@ -7226,7 +7227,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Lemma 4L(a)}}% +\subsection{\pending{Lemma 4L(a)}}% \hyperlabel{sub:lemma-4l-a} \begin{lemma}[4L(a)] @@ -7294,7 +7295,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Lemma 4L(b)}}% +\subsection{\pending{Lemma 4L(b)}}% \hyperlabel{sub:lemma-4l-b} \begin{lemma}[4L(b)] @@ -7577,7 +7578,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Theorem 4N}}% +\subsection{\pending{Theorem 4N}}% \hyperlabel{sub:theorem-4n} \begin{theorem}[4N] @@ -7695,7 +7696,7 @@ Show that $<_L$ is a linear ordering on $A \times B$. \end{proof} -\subsection{\verified{Corollary 4P}}% +\subsection{\pending{Corollary 4P}}% \hyperlabel{sub:corollary-4p} \begin{corollary}[4P] @@ -8320,7 +8321,7 @@ Complete the proof of \nameref{sub:theorem-4k-5}. \end{proof} -\subsection{\verified{Exercise 4.17}}% +\subsection{\pending{Exercise 4.17}}% \hyperlabel{sub:exercise-4.17} Prove that $m^{n+p} = m^n \cdot m^p$.