Enderton. Reorder theorems in Lean modules and add set/logic prompts.

Bookshelf/Apostol/Chapter_1_11.lean

@@ -8,26 +8,21 @@ namespace Apostol.Chapter_1_11
 
 open BigOperators
 
-/-! ## Exercise 4
+/-- #### Exercise 4a
-
-Prove that the greatest-integer function has the properties indicated.
--/
-
-/-- ### Exercise 4a
 
 `⌊x + n⌋ = ⌊x⌋ + n` for every integer `n`.
 -/
 theorem exercise_4a (x : ℝ) (n : ℤ) : ⌊x + n⌋ = ⌊x⌋ + n :=
   Int.floor_add_int x n
 
-/-- ### Exercise 4b.1
+/-- #### Exercise 4b.1
 
 `⌊-x⌋ = -⌊x⌋` if `x` is an integer.
 -/
 theorem exercise_4b_1 (x : ℤ) : ⌊-x⌋ = -⌊x⌋ := by
   simp only [Int.floor_int, id_eq]
 
-/-- ### Exercise 4b.2
+/-- #### Exercise 4b.2
 
 `⌊-x⌋ = -⌊x⌋ - 1` otherwise.
 -/
@@ -47,7 +42,7 @@ theorem exercise_4b_2 (x : ℝ) (h : ∃ n : ℤ, x ∈ Set.Ioo ↑n (↑n + (1
   · exact (Set.mem_Ioo.mp hn).left
   · exact le_of_lt (Set.mem_Ico.mp hn').right
 
-/-- ### Exercise 4c
+/-- #### Exercise 4c
 
 `⌊x + y⌋ = ⌊x⌋ + ⌊y⌋` or `⌊x⌋ + ⌊y⌋ + 1`.
 -/
@@ -77,7 +72,7 @@ theorem exercise_4c (x y : ℝ)
       rw [← sub_lt_iff_lt_add', ← sub_sub, add_sub_cancel, add_sub_cancel]
       exact add_lt_add (Int.fract_lt_one x) (Int.fract_lt_one y)
 
-/-- ### Exercise 5
+/-- #### Exercise 5
 
 The formulas in Exercises 4(d) and 4(e) suggest a generalization for `⌊nx⌋`.
 State and prove such a generalization.
@@ -86,7 +81,7 @@ theorem exercise_5 (n : ℕ) (x : ℝ)
   : ⌊n * x⌋ = Finset.sum (Finset.range n) (fun i => ⌊x + i/n⌋) :=
   Real.Floor.floor_mul_eq_sum_range_floor_add_index_div n x
 
-/-- ### Exercise 4d
+/-- #### Exercise 4d
 
 `⌊2x⌋ = ⌊x⌋ + ⌊x + 1/2⌋`
 -/
@@ -99,7 +94,7 @@ theorem exercise_4d (x : ℝ)
   simp
   rw [add_comm]
 
-/-- ### Exercise 4e
+/-- #### Exercise 4e
 
 `⌊3x⌋ = ⌊x⌋ + ⌊x + 1/3⌋ + ⌊x + 2/3⌋`
 -/
@@ -113,7 +108,7 @@ theorem exercise_4e (x : ℝ)
   conv => rhs; rw [← add_rotate']; arg 2; rw [add_comm]
   rw [← add_assoc]
 
-/-- ### Exercise 7b
+/-- #### Exercise 7b
 
 If `a` and `b` are positive integers with no common factor, we have the formula
 `∑_{n=1}^{b-1} ⌊na / b⌋ = ((a - 1)(b - 1)) / 2`. When `b = 1`, the sum on the
@@ -130,7 +125,7 @@ theorem exercise_7b (ha : a > 0) (hb : b > 0) (hp : Nat.coprime a b)
 
 section
 
-/-- ### Exercise 8
+/-- #### Exercise 8
 
 Let `S` be a set of points on the real line. The *characteristic function* of
 `S` is, by definition, the function `Χ` such that `Χₛ(x) = 1` for every `x` in

Bookshelf/Apostol/Chapter_I_03.lean

@@ -489,8 +489,6 @@ theorem forall_mem_le_forall_mem_imp_sup_le_inf (S T : Set ℝ)
     _ < x := hx.right
   simp at this
 
-/-! ## Exercises -/
-
 /-- #### Exercise 1
 
 If `x` and `y` are arbitrary real numbers with `x < y`, prove that there is at

Bookshelf/Enderton/Logic.tex

@@ -88,6 +88,71 @@
   \lean*{Init/Prelude}
     {Prod}
 
+\section{\defined{Tautological Implication}}%
+\hyperlabel{ref:tautological-implication}
+
+  Consider a set $\Sigma$ of \nameref{ref:well-formed-formula}s and another wff
+    $\tau$.
+  $\Sigma$ \textbf{tautologically implies} $\tau$ (written $\Sigma \vDash \tau$)
+    if and only if every \nameref{ref:truth-assignment} for the sentence symbols
+    in $\Sigma$ and $\tau$ that satisfies every member of $\Sigma$ also
+    satisfies $\tau$.
+  If $\Sigma$ is singleton $\{\sigma\}$, then we write "$\sigma \vDash \tau$" in
+    place of "$\{\sigma\} \vDash \tau$."
+
+  If both $\sigma \vDash \tau$ and $\tau \vDash \sigma$, then $\sigma$ and
+    $\tau$ are said to be \textbf{tautologically equivalent} (written
+    $\sigma \vDash \Dashv \tau$).
+
+\section{\defined{Truth Assignment}}%
+\hyperlabel{ref:truth-assignment}
+
+  A \textbf{truth assignment} $v$ for a set $\mathcal{S}$ of sentence symbols is
+    a function $$v \colon \mathcal{S} \rightarrow \{F, T\}$$ assigning either
+    $T$ or $F$ to each symbol in $\mathcal{S}$.
+
+  Let $\bar{\mathcal{S}}$ be the set of \nameref{ref:well-formed-formula}s that
+    can be built up from $\mathcal{S}$ by the five
+    \nameref{ref:formula-building-operations}.
+  We define \textbf{extension} $\bar{v}$ of $v$,
+    $$\bar{v} \colon \bar{\mathcal{S}} \rightarrow \{F, T\},$$
+    as the function that satisfies the following conditions for any
+    $\alpha, \beta \in \mathcal{S}$:
+    \begin{enumerate}[(1)]
+      \setcounter{enumi}{-1}
+      \item For any $A \in \mathcal{S}$, $\bar{v}(A) = v(A)$.
+        (Thus $\bar{v}$ is indeed an extension of $v$.)
+      \item $\bar{v}((\neg\alpha)) = \begin{cases}
+          T & \text{if } \bar{v}(\alpha) = F, \\
+          F & \text{otherwise}.
+        \end{cases}$
+      \item $\bar{v}((\alpha \land \beta)) = \begin{cases}
+          T & \text{if } \bar{v}(\alpha) = T \text{ and } \bar{v}(\beta) = T, \\
+          F & \text{otherwise}.
+        \end{cases}$
+      \item $\bar{v}((\alpha \lor \beta)) = \begin{cases}
+          T & \text{if } \bar{v}(\alpha) = T \text{ or }
+            \bar{v}(\beta) = T \text{ (or both)}, \\
+          F & \text{otherwise}.
+        \end{cases}$
+      \item $\bar{v}((\alpha \Rightarrow \beta)) = \begin{cases}
+          F & \text{if } \bar{v}(\alpha) = T \text{ and } \bar{v}(\beta) = F, \\
+          T & \text{otherwise}.
+        \end{cases}$
+      \item $\bar{v}((\alpha \Leftrightarrow \beta)) = \begin{cases}
+          T & \text{if } \bar{v}(\alpha) = \bar{v}(\beta), \\
+          F & \text{otherwise}.
+        \end{cases}$
+    \end{enumerate}
+  We say that truth assignment $v$ \textbf{satisfies} $\phi$ if and only if
+    $\bar{v}(\phi) = T$.
+
+  \lean*{Init/Prelude}
+    {True}
+
+  \lean{Init/Prelude}
+    {False}
+
 \section{\defined{Well-Formed Formula}}%
 \hyperlabel{ref:well-formed-formula}
 
@@ -164,16 +229,17 @@
 \hyperlabel{sub:induction-principle-1}
 
   \begin{theorem}
-    If $S$ is a set of wffs containing all the sentence symbols and closed under
+    If $S$ is a set of \nameref{ref:well-formed-formula}s containing all the
-      all five formula-building operations, then $S$ is the set of \textit{all}
+      sentence symbols and closed under all five
-      wffs.
+      \nameref{ref:formula-building-operations}, then $S$ is the set of
+      \textit{all} wffs.
   \end{theorem}
 
   \code{Bookshelf/Enderton/Logic/Chapter\_1}
     {Enderton.Logic.Chapter\_1.Wff.rec}
 
   \begin{proof}
-    We note every \nameref{ref:well-formed-formula} can be characterized by a
+    We note every well-formed formula can be characterized by a
       \nameref{ref:construction-sequence}.
     For natural number $m$, let $P(m)$ be the statement:
       \begin{induction}
@@ -251,7 +317,8 @@
 \hyperlabel{sub:balanced-parentheses}
 
   \begin{lemma}
-    All well-formed formulas have an equal number of left and right parentheses.
+    All \nameref{ref:well-formed-formula}s have an equal number of left and
+      right parentheses.
   \end{lemma}
 
   \begin{proof}
@@ -300,8 +367,8 @@
 \hyperlabel{sub:parentheses-count}
 
   \begin{lemma}
-    Let $\phi$ be a well-formed formula and $c$ be the number of places at which
+    Let $\phi$ be a \nameref{ref:well-formed-formula} and $c$ be the number of
-      a sentential connective symbol exists.
+      places at which a sentential connective symbol exists.
     Then there is $2c$ parentheses in $\phi$.
   \end{lemma}
 
@@ -350,6 +417,36 @@
 
   \end{proof}
 
+\section{Truth Assignments}%
+\hyperlabel{sec:truth-assignments}
+
+\subsection{\sorry{Theorem 12A}}%
+\hyperlabel{sub:theorem-12a}
+
+  \begin{theorem}[12A]
+    For any \nameref{ref:truth-assignment} $v$ for a set $\mathcal{S}$ there is
+      a unique extension
+      $\bar{v} \colon \bar{\mathcal{S}} \rightarrow \{F, T\}$.
+  \end{theorem}
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Compactness Theorem}}%
+\hyperlabel{sub:compactness-theorem}
+
+  \begin{theorem}
+    Let $\Sigma$ be an infinite set of \nameref{ref:well-formed-formula}s such
+      that for any finite subset $\Sigma_0$ of $\Sigma$, there is a
+      \nameref{ref:truth-assignment} that satisfies every member of $\Sigma_0$.
+    Then there is a truth assignment that satisfies every member of $\Sigma$.
+  \end{theorem}
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
 \section{Exercises 1}%
 \hyperlabel{sec:exercises-1}
 
@@ -699,4 +796,300 @@
 
   \end{proof}
 
+\subsection{\sorry{Exercise 1.2.1}}%
+\hyperlabel{sub:exercise-1.2.1}
+
+  Show that neither of the following two formulas tautologically implies the
+    other:
+    \begin{gather*}
+      (A \Leftrightarrow (B \Leftrightarrow C)), \\
+      ((A \land (B \land C)) \lor ((\neg A) \land ((\neg B) \land (\neg C)))).
+    \end{gather*}
+  \textit{Suggestion}: Only two \nameref{ref:truth-assignment}s are needed, not
+    eight.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.2a}}%
+\hyperlabel{sub:exercise-1.2.2a}
+
+  Is $(((P \Rightarrow Q) \Rightarrow P) \Rightarrow P)$ a tautology?
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.2b}}%
+\hyperlabel{sub:exercise-1.2.2b}
+
+  Define $\sigma_k$ recursively as follows: $\sigma_0 = (P \Rightarrow Q)$ and
+    $\sigma_{k + 1} = (\sigma_k \Rightarrow P)$. For which values of $k$ is
+    $\sigma_k$ a tautology? (Part (a) corresponds to $k = 2$.)
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.3a}}%
+\hyperlabel{sub:exercise-1.2.3a}
+
+  Determine whether or not $((P \Rightarrow Q) \lor (Q \Rightarrow P))$ is a
+    tautology.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.3b}}%
+\hyperlabel{sub:exercise-1.2.3b}
+
+  Determine whether or not $((P \land Q) \Rightarrow R)$ tautologically implies
+    $((P \Rightarrow R) \lor (Q \Rightarrow R))$.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.4}}%
+\hyperlabel{sub:exercise-1.2.4}
+
+  Show that the following hold:
+    \begin{enumerate}[(a)]
+      \item $\Sigma; \alpha \vDash \beta$ iff
+        $\Sigma \vDash (\alpha \Rightarrow \beta)$.
+      \item $\alpha \vDash \Dashv \beta$ iff
+        $\vDash (\alpha \Leftrightarrow \beta)$.
+    \end{enumerate}
+  (Recall that $\Sigma; \alpha = \Sigma \cup \{\alpha\}$, the set $\Sigma$
+    together with the one possibly new member $\alpha$.)
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.5}}%
+\hyperlabel{sub:exercise-1.2.5}
+
+  Prove or refute each of the following assertions:
+    \begin{enumerate}[(a)]
+      \item If either $\Sigma \vDash \alpha$ or $\Sigma \vDash \beta$, then
+        $\Sigma \vDash (\alpha \lor \beta)$.
+      \item If $\Sigma \vDash (\alpha \lor \beta)$, then either
+        $\Sigma \vDash \alpha$ or $\Sigma \vDash \beta$.
+    \end{enumerate}
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.6a}}%
+\hyperlabel{sub:exercise-1.2.6a}
+
+  Show that if $v_1$ and $v_2$ are \nameref{ref:truth-assignment}s which agree
+    on all the sentence symbols in the wff $\alpha$, then
+    $\bar{v}_1(\alpha) = \bar{v}_2(\alpha)$.
+  Use the \nameref{sub:induction-principle-1}.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.6b}}%
+\hyperlabel{sub:exercise-1.2.6b}
+
+  Let $\mathcal{S}$ be a set of sentence symbols that includes those in $\Sigma$
+    and $\tau$ (and possibly more).
+  Show that $\Sigma \vDash \tau$ iff every truth assignment for $\mathcal{S}$
+    which satisfies every member of $\Sigma$ also satisfies $\tau$.
+  (This is an easy consequence of part (a). The point of part (b) is that we do
+    not need to worry aboutgetting the domain of a truth assignment
+    \textit{exactly} perfect, as long as it is big enough. For example, one
+    option would be always to use truth assignments on the set of \textit{all}
+    sentence symbols. The drawback is that these are infinite objects, and there
+    are a great many -- uncountably many -- of them.)
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.7}}%
+\hyperlabel{sub:exercise-1.2.7}
+
+  You are in a land inhabited by people who either always tell the truth or
+    always tell falsehoods.
+  You come to a fork in the road and you need to know which fork leads to the
+    capital.
+  There is a local resident there, but he has time only to reply to one
+    yes-or-no question.
+  What one question should you ask so as to learn which fork to take?
+  \textit{Suggestion}: Make a table.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.8}}%
+\hyperlabel{sub:exercise-1.2.8}
+
+  (Substitution) Consider a suquence $\alpha_1, \alpha_2, \ldots$ of wffs.
+  For each wff $\phi$ let $\phi^*$ be the result of replacing the sentence
+    symbol $A_n$ by $\alpha_n$ for each $n$.
+
+\subsubsection{\sorry{Exercise 1.2.8a}}%
+\hyperlabel{ssub:exercise-1.2.8a}
+
+  Let $v$ be a truth assignment for the set of all sentence symbols; define $u$
+    to be the truth assignment for which $u(A_n) = \bar{v}(\alpha_n)$.
+  Show that $\bar{u}(\phi) = \bar{v}(\phi^*)$.
+  Use the induction principle.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsubsection{\sorry{Exercise 1.2.8b}}%
+\hyperlabel{ssub:exercise-1.2.8b}
+
+  Show that if $\phi$ is a tautology, then so is $\phi^*$.
+  (For example, one of our selected tautologies is
+    $((A \land B) \Leftrightarrow (B \land A))$. From this we can conclude, by
+    substitution, that
+    $((\alpha \land \beta) \Leftrightarrow (\beta \land \alpha))$ is a
+    tautology, for any wffs $\alpha$ and $\beta$.)
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.9}}%
+\hyperlabel{sub:exercise-1.2.9}
+
+  (Duality) Let $\alpha$ be a wff whose only connective symbols are $\land$,
+    $\lor$, and $\neg$.
+  Let $\alpha^*$ be the result of interchanging $\land$ and $\lor$ and replacing
+    each sentence symbol by its negation.
+  Show that $\alpha^*$ is tautologically equivalent to $(\neg \alpha)$.
+  Use the \nameref{sub:induction-principle-1}.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.10}}%
+\hyperlabel{sub:exercise-1.2.10}
+
+  Say that a set $\Sigma_1$ of wffs is \textit{equivalent} to a set $\Sigma_2$
+    of wffs iff for any wff $\alpha$, we have $\Sigma_1 \vDash \alpha$ iff
+    $\Sigma_2 \vDash \alpha$.
+  A set $\Sigma$ is \textit{independent} iff no member of $\Sigma$ is
+    tautologically implied by the remaining members in $\Sigma$.
+  Show that the following hold.
+
+\subsubsection{\sorry{Exercise 1.2.10a}}%
+\hyperlabel{ssub:exercise-1.2.10a}
+
+  A finite set of wffs has an independent equivalent subset.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsubsection{\sorry{Exercise 1.2.10b}}%
+\hyperlabel{ssub:exercise-1.2.10b}
+
+  An infinite set need not have an independent equivalent subset.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsubsection{\sorry{Exercise 1.2.10c}}%
+\hyperlabel{ssub:exercise-1.2.10c}
+
+  Let $\Sigma = \{\sigma_0, \sigma_1, \ldots\}$; show that there is an
+    independent equivalent set $\Sigma'$.
+  (By part (b), we cannot hope to have $\Sigma' \subseteq \Sigma$ in general.)
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.11}}%
+\hyperlabel{sub:exercise-1.2.11}
+
+  Show that a truth assignment $v$ satisfies the wff
+    $$(\cdots (A_1 \Leftrightarrow A_2)
+      \Leftrightarrow \cdots \Leftrightarrow A_n)$$
+    iff $v(A_i) = F$ for an even number of $i$'s, $1 \leq i \leq n$.
+  (By the associative law for $\Leftrightarrow$, the placement of the
+    parentheses is not crucial.)
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.12}}%
+\hyperlabel{sub:exercise-1.2.12}
+
+  There are three suspects for a murder: Adams, Brown, and Clark.
+  Adams says "I didn't do it. The victim was an old acquaintance of Brown's.
+    But Clark hated him."
+  Brown states "I didn't do it. I didn't even know the guy. Besides I was out of
+    town all that week."
+  Clark says "I didn't do it. I saw both ADams and Brown downtown with the
+    victim that day; one of them must have done it."
+  Assume that the two innocent men are telling the truth, but that the guilty
+    man might not be.
+  Who did it?
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.13}}%
+\hyperlabel{sub:exercise-1.2.13}
+
+  An advertisement for a tennis magazine states, "If I'm not playing tennis,
+    I'm watching tennis. And if I'm not watching tennis, I'm reading about
+    tennis."
+  We can assume that the speaker cannot do more than one of these activities at
+    a time.
+  What is the speaker doing?
+  (Translate the given sentences into our formal language; consider the possible
+    truth assignments.)
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.14}}%
+\hyperlabel{sub:exercise-1.2.14}
+
+  Let $\mathcal{S}$ be the set of all sentence symbols, and assume that
+    $v \colon \mathcal{S} \rightarrow \{F, T\}$ is a truth assignment.
+  Show there is \textit{at most} one extension $\bar{v}$ meeting conditions 0-5
+    listed at the beginning of this section.
+  (Suppose that $\bar{v}_1$ and $\bar{v}_2$ are both such extensions. Use the
+    \nameref{sub:induction-principle-1} to show that $\bar{v}_1 = \bar{v}_2$.
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
+\subsection{\sorry{Exercise 1.2.15}}%
+\hyperlabel{sub:exercise-1.2.15}
+
+  Of the following three formulas, which tautologically implies which?
+    \begin{enumerate}[(a)]
+      \item $(A \Leftrightarrow B)$
+      \item $(\neg((A \Rightarrow B) \Rightarrow (\neg(B \Rightarrow A))))$
+      \item $(((\neg A) \lor B) \land (A \lor (\neg B)))$
+    \end{enumerate}
+
+  \begin{proof}
+    TODO
+  \end{proof}
+
 \end{document}

Bookshelf/Enderton/Set.tex

@@ -213,11 +213,9 @@
     \textbf{maps $A$ into $B$} (written $F \colon A \rightarrow B$) iff $F$ is a
     function, $\dom{F} = A$, and $\ran{F} \subseteq B$.
   If $\ran{F} = B$, then $F$ is a function from \textbf{$A$ onto $B$}.
-
   A function $F$ is \textbf{one-to-one} iff for each $y \in \ran{F}$ there is
     only one $x$ such that $xFy$.
   One-to-one functions are sometimes called \textbf{injections}.
-
   A one-to-one function from $A$ onto $B$ is a
     \textbf{one-to-one correspondence} between $A$ and $B$.
 
@@ -6173,7 +6171,7 @@
 \hyperlabel{sub:theorem-4i}
 
   \begin{theorem}[4I]
-    For natural numbers $m$ and $n$,
+    For \nameref{ref:natural-number}s $m$ and $n$,
       \begin{align}
         m + 0 & = m, \hyperlabel{sub:theorem-4i-eq1} \\
         m + n^+ & = (m + n)^+. \hyperlabel{sub:theorem-4i-eq2}
@@ -6328,7 +6326,7 @@
 \hyperlabel{sub:theorem-4k-1}
 
   \begin{theorem}[4K-1]
-    Associative law for addition.
+    Associative law for \nameref{ref:addition}.
     For $m, n, p \in \omega$, $$m + (n + p) = (m + n) + p.$$
   \end{theorem}
 
@@ -6385,7 +6383,7 @@
 \hyperlabel{sub:theorem-4k-2}
 
   \begin{theorem}[4K-2]
-    Commutative law for addition.
+    Commutative law for \nameref{ref:addition}.
     For $m, n \in \omega$, $$m + n = n + m.$$
   \end{theorem}
 
@@ -6716,7 +6714,7 @@
 \hyperlabel{sub:theorem-4k-5}
 
   \begin{theorem}[4K-5]
-    Commutative law for multiplication.
+    Commutative law for \nameref{ref:multiplication}.
     For $m, n \in \omega$, $$m \cdot n = n \cdot m.$$
   \end{theorem}
 
@@ -6777,7 +6775,7 @@
 \hyperlabel{sub:theorem-4k-4}
 
   \begin{theorem}[4K-4]
-    Associative law for multiplication.
+    Associative law for \nameref{ref:multiplication}.
     For $m, n, p \in \omega$, $$m \cdot (n \cdot p) = (m \cdot n) \cdot p.$$
   \end{theorem}
 
@@ -6859,7 +6857,8 @@
 \hyperlabel{sub:members-natural-numbers}
 
   \begin{lemma}
-    Every natural number is the set of all smaller natural numbers.
+    Every \nameref{ref:natural-number} is the set of all smaller natural
+      numbers.
   \end{lemma}
 
   \begin{proof}
@@ -6874,7 +6873,8 @@
 \hyperlabel{sub:lemma-4l-a}
 
   \begin{lemma}[4L(a)]
-    For any natural numbers $m$ and $n$, $$m \in n \iff m^+ \in n^+.$$
+    For any \nameref{ref:natural-number}s $m$ and $n$,
+      $$m \in n \iff m^+ \in n^+.$$
   \end{lemma}
 
   \lean{Std/Data/Nat/Lemmas}{Nat.succ\_lt\_succ\_iff}
@@ -6940,7 +6940,7 @@
 \hyperlabel{sub:lemma-4l-b}
 
   \begin{lemma}[4L(b)]
-    No natural number is a member of itself.
+    No \nameref{ref:natural-number} is a member of itself.
   \end{lemma}
 
   \code{Bookshelf/Enderton/Set/Chapter\_4}
@@ -6987,7 +6987,7 @@
 \hyperlabel{sub:zero-least-natural-number}
 
   \begin{lemma}
-    For every natural number $n \neq 0$, $0 \in n$.
+    For every \nameref{ref:natural-number} $n \neq 0$, $0 \in n$.
   \end{lemma}
 
   \code{Bookshelf/Enderton/Set/Chapter\_4}
@@ -7032,8 +7032,8 @@
 \hyperlabel{sub:trichotomy-law-natural-numbers}
 
   \begin{theorem}
-    For any natural numbers $m$ and $n$, exactly one of the three conditions
+    For any \nameref{ref:natural-number}s $m$ and $n$, exactly one of the three
-      $$m \in n, \quad m = n, \quad n \in m$$ holds.
+      conditions $$m \in n, \quad m = n, \quad n \in m$$ holds.
   \end{theorem}
 
   \lean{Mathlib/Order/RelClasses}{IsAsymm}
@@ -7112,12 +7112,12 @@
 \hyperlabel{sub:linear-ordering-natural-numbers}
 
   \begin{theorem}
-    Relation
+    \nameref{ref:relation}
       \begin{equation}
         \hyperlabel{sub:linear-ordering-natural-numbers-eq1}
         \in_\omega = \{\tuple{m, n} \in \omega \times \omega \mid m \in n\}
       \end{equation}
-      is a linear ordering on $\omega$.
+      is a \nameref{ref:linear-ordering} on $\omega$.
   \end{theorem}
 
   \lean{Mathlib/Init/Algebra/Order}
@@ -7125,9 +7125,8 @@
 
   \begin{proof}
 
-    By definition, \eqref{sub:linear-ordering-natural-numbers-eq1} is a
+    By definition, \eqref{sub:linear-ordering-natural-numbers-eq1} is a linear
-      \nameref{ref:linear-ordering} on $\omega$ if it is (i) transitive and
+      ordering on $\omega$ if it is (i) transitive and (ii) trichotomous.
-      (ii) trichotomous.
 
     \paragraph{(i)}%
 
@@ -8510,7 +8509,7 @@
 \hyperlabel{sub:theorem-6b}
 
   \begin{theorem}[6B]
-    No set is equinumerous to its powerset.
+    No set is \nameref{ref:equinumerous} to its powerset.
   \end{theorem}
 
   \begin{proof}

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -15,6 +15,8 @@ Relations and Functions
 
 namespace Enderton.Set.Chapter_3
 
+open Set.Relation
+
 /-- #### Lemma 3B
 
 If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`.
@@ -25,203 +27,6 @@ lemma lemma_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
   have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
   exact Set.mem_mem_imp_pair_subset hxs hxys
 
-/-- #### Exercise 3.1
-
-Suppose that we attempted to generalize the Kuratowski definitions of ordered
-pairs to ordered triples by defining
-```
-⟨x, y, z⟩* = {{x}, {x, y}, {x, y, z}}.open Set
-
-```
-Show that this definition is unsuccessful by giving examples of objects `u`,
-`v`, `w`, `x`, `y`, `z` with `⟨x, y, z⟩* = ⟨u, v, w⟩*` but with either `y ≠ v`
-or `z ≠ w` (or both).
--/
-theorem exercise_3_1 {x y z u v w : ℕ}
-  (hx : x = 1) (hy : y = 1) (hz : z = 2)
-  (hu : u = 1) (hv : v = 2) (hw : w = 2)
-  : ({{x}, {x, y}, {x, y, z}} : Set (Set ℕ)) = {{u}, {u, v}, {u, v, w}}
-  ∧ y ≠ v := by
-  apply And.intro
-  · rw [hx, hy, hz, hu, hv, hw]
-    simp
-  · rw [hy, hv]
-    simp only
-
-/-- #### Exercise 3.2a
-
-Show that `A × (B ∪ C) = (A × B) ∪ (A × C)`.
--/
-theorem exercise_3_2a {A : Set α} {B C : Set β}
-  : Set.prod A (B ∪ C) = (Set.prod A B) ∪ (Set.prod A C) := by
-  calc Set.prod A (B ∪ C)
-    _ = { p | p.1 ∈ A ∧ p.2 ∈ B ∪ C } := rfl
-    _ = { p | p.1 ∈ A ∧ (p.2 ∈ B ∨ p.2 ∈ C) } := rfl
-    _ = { p | (p.1 ∈ A ∧ p.2 ∈ B) ∨ (p.1 ∈ A ∧ p.2 ∈ C) } := by
-      ext x
-      rw [Set.mem_setOf_eq]
-      conv => lhs; rw [and_or_left]
-    _ = { p | p ∈ Set.prod A B ∨ (p ∈ Set.prod A C) } := rfl
-    _ = (Set.prod A B) ∪ (Set.prod A C) := rfl
-
-/-- #### Exercise 3.2b
-
-Show that if `A × B = A × C` and `A ≠ ∅`, then `B = C`.
--/
-theorem exercise_3_2b {A : Set α} {B C : Set β}
-  (h : Set.prod A B = Set.prod A C) (hA : Set.Nonempty A)
-  : B = C := by
-  by_cases hB : Set.Nonempty B
-  · rw [Set.Subset.antisymm_iff]
-    have ⟨a, ha⟩ := hA
-    apply And.intro
-    · show ∀ t, t ∈ B → t ∈ C
-      intro t ht
-      have : (a, t) ∈ Set.prod A B := ⟨ha, ht⟩
-      rw [h] at this
-      exact this.right
-    · show ∀ t, t ∈ C → t ∈ B
-      intro t ht
-      have : (a, t) ∈ Set.prod A C := ⟨ha, ht⟩
-      rw [← h] at this
-      exact this.right
-  · have nB : B = ∅ := Set.not_nonempty_iff_eq_empty.mp hB
-    rw [nB, Set.prod_right_emptyset_eq_emptyset, Set.ext_iff] at h
-    rw [nB]
-    by_contra nC
-    have ⟨a, ha⟩ := hA
-    have ⟨c, hc⟩ := Set.nonempty_iff_ne_empty.mpr (Ne.symm nC)
-    exact (h (a, c)).mpr ⟨ha, hc⟩
-
-/-- #### Exercise 3.3
-
-Show that `A × ⋃ 𝓑 = ⋃ {A × X | X ∈ 𝓑}`.
--/
-theorem exercise_3_3 {A : Set (Set α)} {𝓑 : Set (Set β)}
-  : Set.prod A (⋃₀ 𝓑) = ⋃₀ {Set.prod A X | X ∈ 𝓑} := by
-  calc Set.prod A (⋃₀ 𝓑)
-    _ = { p | p.1 ∈ A ∧ p.2 ∈ ⋃₀ 𝓑} := rfl
-    _ = { p | p.1 ∈ A ∧ ∃ b ∈ 𝓑, p.2 ∈ b } := rfl
-    _ = { p | ∃ b ∈ 𝓑, p.1 ∈ A ∧ p.2 ∈ b } := by
-      ext x
-      rw [Set.mem_setOf_eq]
-      apply Iff.intro
-      · intro ⟨h₁, b, h₂⟩
-        exact ⟨b, h₂.left, h₁, h₂.right⟩
-      · intro ⟨b, h₁, h₂, h₃⟩
-        exact ⟨h₂, b, h₁, h₃⟩
-    _ = ⋃₀ { Set.prod A p | p ∈ 𝓑 } := by
-      ext x
-      rw [Set.mem_setOf_eq]
-      unfold Set.sUnion sSup Set.instSupSetSet
-      simp only [Set.mem_setOf_eq, exists_exists_and_eq_and]
-      apply Iff.intro
-      · intro ⟨b, h₁, h₂, h₃⟩
-        exact ⟨b, h₁, h₂, h₃⟩
-      · intro ⟨b, h₁, h₂, h₃⟩
-        exact ⟨b, h₁, h₂, h₃⟩
-
-/-- #### Exercise 3.5a
-
-Assume that `A` and `B` are given sets, and show that there exists a set `C`
-such that for any `y`,
-```
-y ∈ C ↔ y = {x} × B for some x in A.
-```
-In other words, show that `{{x} × B | x ∈ A}` is a set.
--/
-theorem exercise_3_5a {A : Set α} {B : Set β}
-  : ∃ C : Set (Set (α × β)),
-      y ∈ C ↔ ∃ x ∈ A, y = Set.prod {x} B := by
-  let C := {y ∈ 𝒫 (Set.prod A B) | ∃ a ∈ A, ∀ x, (x ∈ y ↔ ∃ b ∈ B, x = (a, b))}
-  refine ⟨C, ?_⟩
-  apply Iff.intro
-  · intro hC
-    simp only [Set.mem_setOf_eq] at hC
-    have ⟨_, ⟨a, ⟨ha, h⟩⟩⟩ := hC
-    refine ⟨a, ⟨ha, ?_⟩⟩
-    ext x
-    apply Iff.intro
-    · intro hxy
-      unfold Set.prod
-      simp only [Set.mem_singleton_iff, Set.mem_setOf_eq]
-      have ⟨b, ⟨hb, hx⟩⟩ := (h x).mp hxy
-      rw [Prod.ext_iff] at hx
-      simp only at hx
-      rw [← hx.right] at hb
-      exact ⟨hx.left, hb⟩
-    · intro hx
-      simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at hx
-      have := (h (a, x.snd)).mpr ⟨x.snd, ⟨hx.right, rfl⟩⟩
-      have hxab : x = (a, x.snd) := by
-        ext <;> simp
-        exact hx.left
-      rwa [← hxab] at this
-  · intro ⟨x, ⟨hx, hy⟩⟩
-    show y ∈ 𝒫 Set.prod A B ∧ ∃ a, a ∈ A ∧
-           ∀ (x : α × β), x ∈ y ↔ ∃ b, b ∈ B ∧ x = (a, b)
-    apply And.intro
-    · simp only [Set.mem_powerset_iff]
-      rw [hy]
-      unfold Set.prod
-      simp only [
-        Set.mem_singleton_iff,
-        Set.setOf_subset_setOf,
-        and_imp,
-        Prod.forall
-      ]
-      intro a b ha hb
-      exact ⟨by rw [ha]; exact hx, hb⟩
-    · refine ⟨x, ⟨hx, ?_⟩⟩
-      intro p
-      apply Iff.intro
-      · intro hab
-        rw [hy] at hab
-        unfold Set.prod at hab
-        simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at hab
-        exact ⟨p.2, ⟨hab.right, by ext; exact hab.left; simp⟩⟩
-      · intro ⟨b, ⟨hb, hab⟩⟩
-        rw [hy]
-        unfold Set.prod
-        simp only [Set.mem_singleton_iff, Set.mem_setOf_eq]
-        rw [Prod.ext_iff] at hab
-        simp only at hab
-        rw [hab.right]
-        exact ⟨hab.left, hb⟩
-
-/-- #### Exercise 3.5b
-
-With `A`, `B`, and `C` as above, show that `A × B = ∪ C`.
--/
-theorem exercise_3_5b {A : Set α} (B : Set β)
-  : Set.prod A B = ⋃₀ {Set.prod ({x} : Set α) B | x ∈ A} := by
-  rw [Set.Subset.antisymm_iff]
-  apply And.intro
-  · show ∀ t, t ∈ Set.prod A B → t ∈ ⋃₀ {Set.prod {x} B | x ∈ A}
-    intro t h
-    simp only [Set.mem_setOf_eq] at h
-    unfold Set.sUnion sSup Set.instSupSetSet
-    simp only [Set.mem_setOf_eq, exists_exists_and_eq_and]
-    unfold Set.prod at h
-    simp only [Set.mem_setOf_eq] at h
-    refine ⟨t.fst, ⟨h.left, ?_⟩⟩
-    unfold Set.prod
-    simp only [Set.mem_singleton_iff, Set.mem_setOf_eq, true_and]
-    exact h.right
-  · show ∀ t, t ∈ ⋃₀ {Set.prod {x} B | x ∈ A} → t ∈ Set.prod A B
-    unfold Set.prod
-    intro t ht
-    simp only [
-      Set.mem_singleton_iff,
-      Set.mem_sUnion,
-      Set.mem_setOf_eq,
-      exists_exists_and_eq_and
-    ] at ht
-    have ⟨a, ⟨h, ⟨ha, hb⟩⟩⟩ := ht
-    simp only [Set.mem_setOf_eq]
-    rw [← ha] at h
-    exact ⟨h, hb⟩
-
 /-- #### Theorem 3D
 
 If `⟨x, y⟩ ∈ A`, then `x` and `y` belong to `⋃ ⋃ A`.
@@ -234,209 +39,6 @@ theorem theorem_3d {A : Set (Set (Set α))} (h : OrderedPair x y ∈ A)
   have : {x, y} ⊆ ⋃₀ ⋃₀ A := Chapter_2.exercise_2_3 {x, y} hq
   exact ⟨this (by simp), this (by simp)⟩
 
-section Relation
-
-open Set.Relation
-
-/-- #### Exercise 3.6
-
-Show that a set `A` is a relation **iff** `A ⊆ dom A × ran A`.
--/
-theorem exercise_3_6 {A : Set.HRelation α β}
-  : A ⊆ Set.prod (dom A) (ran A) := by
-  show ∀ t, t ∈ A → t ∈ Set.prod (Prod.fst '' A) (Prod.snd '' A)
-  intro (a, b) ht
-  unfold Set.prod
-  simp only [
-    Set.mem_image,
-    Prod.exists,
-    exists_and_right,
-    exists_eq_right,
-    Set.mem_setOf_eq
-  ]
-  exact ⟨⟨b, ht⟩, ⟨a, ht⟩⟩
-
-/-- #### Exercise 3.7
-
-Show that if `R` is a relation, then `fld R = ⋃ ⋃ R`.
--/
-theorem exercise_3_7 {R : Set.Relation α}
-  : R.fld = ⋃₀ ⋃₀ R.toOrderedPairs := by
-  let img := R.toOrderedPairs
-  rw [Set.Subset.antisymm_iff]
-  apply And.intro
-  · show ∀ x, x ∈ R.fld → x ∈ ⋃₀ ⋃₀ img
-    intro x hx
-    apply Or.elim hx
-    · intro hd
-      unfold Set.Relation.dom Prod.fst at hd
-      simp only [
-        Set.mem_image, Prod.exists, exists_and_right, exists_eq_right
-      ] at hd
-      have ⟨y, hp⟩ := hd
-      have hm : OrderedPair x y ∈ Set.image (fun p => OrderedPair p.1 p.2) R := by
-        unfold Set.image
-        simp only [Prod.exists, Set.mem_setOf_eq]
-        exact ⟨x, ⟨y, ⟨hp, rfl⟩⟩⟩
-      unfold OrderedPair at hm
-      have : {x} ∈ ⋃₀ img := Chapter_2.exercise_2_3 {{x}, {x, y}} hm (by simp)
-      exact (Chapter_2.exercise_2_3 {x} this) (show x ∈ {x} by rfl)
-    · intro hr
-      unfold Set.Relation.ran Prod.snd at hr
-      simp only [Set.mem_image, Prod.exists, exists_eq_right] at hr
-      have ⟨t, ht⟩ := hr
-      have hm : OrderedPair t x ∈ Set.image (fun p => OrderedPair p.1 p.2) R := by
-        simp only [Set.mem_image, Prod.exists]
-        exact ⟨t, ⟨x, ⟨ht, rfl⟩⟩⟩
-      unfold OrderedPair at hm
-      have : {t, x} ∈ ⋃₀ img := Chapter_2.exercise_2_3 {{t}, {t, x}} hm
-        (show {t, x} ∈ {{t}, {t, x}} by simp)
-      exact Chapter_2.exercise_2_3 {t, x} this (show x ∈ {t, x} by simp)
-
-  · show ∀ t, t ∈ ⋃₀ ⋃₀ img → t ∈ Set.Relation.fld R
-    intro t ht
-    have ⟨T, hT⟩ : ∃ T ∈ ⋃₀ img, t ∈ T := ht
-    have ⟨T', hT'⟩ : ∃ T' ∈ img, T ∈ T' := hT.left
-    dsimp only at hT'
-    unfold Set.Relation.toOrderedPairs at hT'
-    simp only [Set.mem_image, Prod.exists] at hT'
-    have ⟨x, ⟨y, ⟨p, hp⟩⟩⟩ := hT'.left
-    have hr := hT'.right
-    rw [← hp] at hr
-    unfold OrderedPair at hr
-    simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at hr
-
-    -- Use `exercise_6_6` to prove that if `t = x` then `t ∈ dom R` and if
-    -- `t = y` then `t ∈ ran R`.
-    have hxy_mem : t = x ∨ t = y → t ∈ Set.Relation.fld R := by
-      intro ht
-      have hz : R ⊆ Set.prod (dom R) (ran R) := exercise_3_6
-      have : (x, y) ∈ Set.prod (dom R) (ran R) := hz p
-      unfold Set.prod at this
-      simp at this
-      apply Or.elim ht
-      · intro ht'
-        rw [← ht'] at this
-        exact Or.inl this.left
-      · intro ht'
-        rw [← ht'] at this
-        exact Or.inr this.right
-
-    -- Eliminate `T = {x} ∨ T = {x, y}`.
-    apply Or.elim hr
-    · intro hx
-      have := hT.right
-      rw [hx] at this
-      simp only [Set.mem_singleton_iff] at this
-      exact hxy_mem (Or.inl this)
-    · intro hxy
-      have := hT.right
-      rw [hxy] at this
-      simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at this
-      exact hxy_mem this
-
-/-- #### Exercise 3.8 (i)
-
-Show that for any set `𝓐`:
-```
-dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
-```
--/
-theorem exercise_3_8_i {A : Set (Set.HRelation α β)}
-  : dom (⋃₀ A) = ⋃₀ { dom R | R ∈ A } := by
-  ext x
-  unfold dom Prod.fst
-  simp only [
-    Set.mem_image,
-    Set.mem_sUnion,
-    Prod.exists,
-    exists_and_right,
-    exists_eq_right,
-    Set.mem_setOf_eq,
-    exists_exists_and_eq_and
-  ]
-  apply Iff.intro
-  · intro ⟨y, t, ht, hx⟩
-    exact ⟨t, ht, y, hx⟩
-  · intro ⟨t, ht, y, hx⟩
-    exact ⟨y, t, ht, hx⟩
-
-/-- #### Exercise 3.8 (ii)
-
-Show that for any set `𝓐`:
-```
-ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
-```
--/
-theorem exercise_3_8_ii {A : Set (Set.HRelation α β)}
-  : ran (⋃₀ A) = ⋃₀ { ran R | R ∈ A } := by
-  ext x
-  unfold ran Prod.snd
-  simp only [
-    Set.mem_image,
-    Set.mem_sUnion,
-    Prod.exists,
-    exists_eq_right,
-    Set.mem_setOf_eq,
-    exists_exists_and_eq_and
-  ]
-  apply Iff.intro
-  · intro ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩
-    exact ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩
-  · intro ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩
-    exact ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩
-
-/-- #### Exercise 3.9 (i)
-
-Discuss the result of replacing the union operation by the intersection
-operation in the preceding problem.
-```
-dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
-```
--/
-theorem exercise_3_9_i {A : Set (Set.HRelation α β)}
-  : dom (⋂₀ A) ⊆ ⋂₀ { dom R | R ∈ A } := by
-  show ∀ x, x ∈ dom (⋂₀ A) → x ∈ ⋂₀ { dom R | R ∈ A }
-  unfold dom Prod.fst
-  simp only [
-    Set.mem_image,
-    Set.mem_sInter,
-    Prod.exists,
-    exists_and_right,
-    exists_eq_right,
-    Set.mem_setOf_eq,
-    forall_exists_index,
-    and_imp,
-    forall_apply_eq_imp_iff₂
-  ]
-  intro _ y hy R hR
-  exact ⟨y, hy R hR⟩
-
-/-- #### Exercise 3.9 (ii)
-
-Discuss the result of replacing the union operation by the intersection
-operation in the preceding problem.
-```
-ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
-```
--/
-theorem exercise_3_9_ii {A : Set (Set.HRelation α β)}
-  : ran (⋂₀ A) ⊆ ⋂₀ { ran R | R ∈ A } := by
-  show ∀ x, x ∈ ran (⋂₀ A) → x ∈ ⋂₀ { ran R | R ∈ A }
-  unfold ran Prod.snd
-  simp only [
-    Set.mem_image,
-    Set.mem_sInter,
-    Prod.exists,
-    exists_and_right,
-    exists_eq_right,
-    Set.mem_setOf_eq,
-    forall_exists_index,
-    and_imp,
-    forall_apply_eq_imp_iff₂
-  ]
-  intro _ y hy R hR
-  exact ⟨y, hy R hR⟩
 
 /-- #### Theorem 3G (i)
 
@@ -729,6 +331,428 @@ theorem corollary_3l_iii {G : Set.HRelation β α} {A B : Set α}
     single_valued_self_iff_single_rooted_inv.mp hG
   exact (theorem_3k_c_ii hG').symm
 
+/-- #### Theorem 3R
+
+Let `R` be a linear ordering on `A`.
+
+(i) There is no `x` for which `xRx`.
+(ii) For distinct `x` and `y` in `A`, either `xRy` or `yRx`.
+-/
+theorem theorem_3r {R : Rel α α} (hR : IsStrictTotalOrder α R)
+  : (∀ x : α, ¬ R x x) ∧ (∀ x y : α, x ≠ y → R x y ∨ R y x) := by
+  apply And.intro
+  · exact hR.irrefl
+  · intro x y h
+    apply Or.elim (hR.trichotomous x y)
+    · intro h₁
+      left
+      exact h₁
+    · intro h₁
+      apply Or.elim h₁
+      · intro h₂
+        exact absurd h₂ h
+      · intro h₂
+        right
+        exact h₂
+
+/-- #### Exercise 3.1
+
+Suppose that we attempted to generalize the Kuratowski definitions of ordered
+pairs to ordered triples by defining
+```
+⟨x, y, z⟩* = {{x}, {x, y}, {x, y, z}}.open Set
+
+```
+Show that this definition is unsuccessful by giving examples of objects `u`,
+`v`, `w`, `x`, `y`, `z` with `⟨x, y, z⟩* = ⟨u, v, w⟩*` but with either `y ≠ v`
+or `z ≠ w` (or both).
+-/
+theorem exercise_3_1 {x y z u v w : ℕ}
+  (hx : x = 1) (hy : y = 1) (hz : z = 2)
+  (hu : u = 1) (hv : v = 2) (hw : w = 2)
+  : ({{x}, {x, y}, {x, y, z}} : Set (Set ℕ)) = {{u}, {u, v}, {u, v, w}}
+  ∧ y ≠ v := by
+  apply And.intro
+  · rw [hx, hy, hz, hu, hv, hw]
+    simp
+  · rw [hy, hv]
+    simp only
+
+/-- #### Exercise 3.2a
+
+Show that `A × (B ∪ C) = (A × B) ∪ (A × C)`.
+-/
+theorem exercise_3_2a {A : Set α} {B C : Set β}
+  : Set.prod A (B ∪ C) = (Set.prod A B) ∪ (Set.prod A C) := by
+  calc Set.prod A (B ∪ C)
+    _ = { p | p.1 ∈ A ∧ p.2 ∈ B ∪ C } := rfl
+    _ = { p | p.1 ∈ A ∧ (p.2 ∈ B ∨ p.2 ∈ C) } := rfl
+    _ = { p | (p.1 ∈ A ∧ p.2 ∈ B) ∨ (p.1 ∈ A ∧ p.2 ∈ C) } := by
+      ext x
+      rw [Set.mem_setOf_eq]
+      conv => lhs; rw [and_or_left]
+    _ = { p | p ∈ Set.prod A B ∨ (p ∈ Set.prod A C) } := rfl
+    _ = (Set.prod A B) ∪ (Set.prod A C) := rfl
+
+/-- #### Exercise 3.2b
+
+Show that if `A × B = A × C` and `A ≠ ∅`, then `B = C`.
+-/
+theorem exercise_3_2b {A : Set α} {B C : Set β}
+  (h : Set.prod A B = Set.prod A C) (hA : Set.Nonempty A)
+  : B = C := by
+  by_cases hB : Set.Nonempty B
+  · rw [Set.Subset.antisymm_iff]
+    have ⟨a, ha⟩ := hA
+    apply And.intro
+    · show ∀ t, t ∈ B → t ∈ C
+      intro t ht
+      have : (a, t) ∈ Set.prod A B := ⟨ha, ht⟩
+      rw [h] at this
+      exact this.right
+    · show ∀ t, t ∈ C → t ∈ B
+      intro t ht
+      have : (a, t) ∈ Set.prod A C := ⟨ha, ht⟩
+      rw [← h] at this
+      exact this.right
+  · have nB : B = ∅ := Set.not_nonempty_iff_eq_empty.mp hB
+    rw [nB, Set.prod_right_emptyset_eq_emptyset, Set.ext_iff] at h
+    rw [nB]
+    by_contra nC
+    have ⟨a, ha⟩ := hA
+    have ⟨c, hc⟩ := Set.nonempty_iff_ne_empty.mpr (Ne.symm nC)
+    exact (h (a, c)).mpr ⟨ha, hc⟩
+
+/-- #### Exercise 3.3
+
+Show that `A × ⋃ 𝓑 = ⋃ {A × X | X ∈ 𝓑}`.
+-/
+theorem exercise_3_3 {A : Set (Set α)} {𝓑 : Set (Set β)}
+  : Set.prod A (⋃₀ 𝓑) = ⋃₀ {Set.prod A X | X ∈ 𝓑} := by
+  calc Set.prod A (⋃₀ 𝓑)
+    _ = { p | p.1 ∈ A ∧ p.2 ∈ ⋃₀ 𝓑} := rfl
+    _ = { p | p.1 ∈ A ∧ ∃ b ∈ 𝓑, p.2 ∈ b } := rfl
+    _ = { p | ∃ b ∈ 𝓑, p.1 ∈ A ∧ p.2 ∈ b } := by
+      ext x
+      rw [Set.mem_setOf_eq]
+      apply Iff.intro
+      · intro ⟨h₁, b, h₂⟩
+        exact ⟨b, h₂.left, h₁, h₂.right⟩
+      · intro ⟨b, h₁, h₂, h₃⟩
+        exact ⟨h₂, b, h₁, h₃⟩
+    _ = ⋃₀ { Set.prod A p | p ∈ 𝓑 } := by
+      ext x
+      rw [Set.mem_setOf_eq]
+      unfold Set.sUnion sSup Set.instSupSetSet
+      simp only [Set.mem_setOf_eq, exists_exists_and_eq_and]
+      apply Iff.intro
+      · intro ⟨b, h₁, h₂, h₃⟩
+        exact ⟨b, h₁, h₂, h₃⟩
+      · intro ⟨b, h₁, h₂, h₃⟩
+        exact ⟨b, h₁, h₂, h₃⟩
+
+/-- #### Exercise 3.5a
+
+Assume that `A` and `B` are given sets, and show that there exists a set `C`
+such that for any `y`,
+```
+y ∈ C ↔ y = {x} × B for some x in A.
+```
+In other words, show that `{{x} × B | x ∈ A}` is a set.
+-/
+theorem exercise_3_5a {A : Set α} {B : Set β}
+  : ∃ C : Set (Set (α × β)),
+      y ∈ C ↔ ∃ x ∈ A, y = Set.prod {x} B := by
+  let C := {y ∈ 𝒫 (Set.prod A B) | ∃ a ∈ A, ∀ x, (x ∈ y ↔ ∃ b ∈ B, x = (a, b))}
+  refine ⟨C, ?_⟩
+  apply Iff.intro
+  · intro hC
+    simp only [Set.mem_setOf_eq] at hC
+    have ⟨_, ⟨a, ⟨ha, h⟩⟩⟩ := hC
+    refine ⟨a, ⟨ha, ?_⟩⟩
+    ext x
+    apply Iff.intro
+    · intro hxy
+      unfold Set.prod
+      simp only [Set.mem_singleton_iff, Set.mem_setOf_eq]
+      have ⟨b, ⟨hb, hx⟩⟩ := (h x).mp hxy
+      rw [Prod.ext_iff] at hx
+      simp only at hx
+      rw [← hx.right] at hb
+      exact ⟨hx.left, hb⟩
+    · intro hx
+      simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at hx
+      have := (h (a, x.snd)).mpr ⟨x.snd, ⟨hx.right, rfl⟩⟩
+      have hxab : x = (a, x.snd) := by
+        ext <;> simp
+        exact hx.left
+      rwa [← hxab] at this
+  · intro ⟨x, ⟨hx, hy⟩⟩
+    show y ∈ 𝒫 Set.prod A B ∧ ∃ a, a ∈ A ∧
+           ∀ (x : α × β), x ∈ y ↔ ∃ b, b ∈ B ∧ x = (a, b)
+    apply And.intro
+    · simp only [Set.mem_powerset_iff]
+      rw [hy]
+      unfold Set.prod
+      simp only [
+        Set.mem_singleton_iff,
+        Set.setOf_subset_setOf,
+        and_imp,
+        Prod.forall
+      ]
+      intro a b ha hb
+      exact ⟨by rw [ha]; exact hx, hb⟩
+    · refine ⟨x, ⟨hx, ?_⟩⟩
+      intro p
+      apply Iff.intro
+      · intro hab
+        rw [hy] at hab
+        unfold Set.prod at hab
+        simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at hab
+        exact ⟨p.2, ⟨hab.right, by ext; exact hab.left; simp⟩⟩
+      · intro ⟨b, ⟨hb, hab⟩⟩
+        rw [hy]
+        unfold Set.prod
+        simp only [Set.mem_singleton_iff, Set.mem_setOf_eq]
+        rw [Prod.ext_iff] at hab
+        simp only at hab
+        rw [hab.right]
+        exact ⟨hab.left, hb⟩
+
+/-- #### Exercise 3.5b
+
+With `A`, `B`, and `C` as above, show that `A × B = ∪ C`.
+-/
+theorem exercise_3_5b {A : Set α} (B : Set β)
+  : Set.prod A B = ⋃₀ {Set.prod ({x} : Set α) B | x ∈ A} := by
+  rw [Set.Subset.antisymm_iff]
+  apply And.intro
+  · show ∀ t, t ∈ Set.prod A B → t ∈ ⋃₀ {Set.prod {x} B | x ∈ A}
+    intro t h
+    simp only [Set.mem_setOf_eq] at h
+    unfold Set.sUnion sSup Set.instSupSetSet
+    simp only [Set.mem_setOf_eq, exists_exists_and_eq_and]
+    unfold Set.prod at h
+    simp only [Set.mem_setOf_eq] at h
+    refine ⟨t.fst, ⟨h.left, ?_⟩⟩
+    unfold Set.prod
+    simp only [Set.mem_singleton_iff, Set.mem_setOf_eq, true_and]
+    exact h.right
+  · show ∀ t, t ∈ ⋃₀ {Set.prod {x} B | x ∈ A} → t ∈ Set.prod A B
+    unfold Set.prod
+    intro t ht
+    simp only [
+      Set.mem_singleton_iff,
+      Set.mem_sUnion,
+      Set.mem_setOf_eq,
+      exists_exists_and_eq_and
+    ] at ht
+    have ⟨a, ⟨h, ⟨ha, hb⟩⟩⟩ := ht
+    simp only [Set.mem_setOf_eq]
+    rw [← ha] at h
+    exact ⟨h, hb⟩
+
+
+/-- #### Exercise 3.6
+
+Show that a set `A` is a relation **iff** `A ⊆ dom A × ran A`.
+-/
+theorem exercise_3_6 {A : Set.HRelation α β}
+  : A ⊆ Set.prod (dom A) (ran A) := by
+  show ∀ t, t ∈ A → t ∈ Set.prod (Prod.fst '' A) (Prod.snd '' A)
+  intro (a, b) ht
+  unfold Set.prod
+  simp only [
+    Set.mem_image,
+    Prod.exists,
+    exists_and_right,
+    exists_eq_right,
+    Set.mem_setOf_eq
+  ]
+  exact ⟨⟨b, ht⟩, ⟨a, ht⟩⟩
+
+/-- #### Exercise 3.7
+
+Show that if `R` is a relation, then `fld R = ⋃ ⋃ R`.
+-/
+theorem exercise_3_7 {R : Set.Relation α}
+  : R.fld = ⋃₀ ⋃₀ R.toOrderedPairs := by
+  let img := R.toOrderedPairs
+  rw [Set.Subset.antisymm_iff]
+  apply And.intro
+  · show ∀ x, x ∈ R.fld → x ∈ ⋃₀ ⋃₀ img
+    intro x hx
+    apply Or.elim hx
+    · intro hd
+      unfold Set.Relation.dom Prod.fst at hd
+      simp only [
+        Set.mem_image, Prod.exists, exists_and_right, exists_eq_right
+      ] at hd
+      have ⟨y, hp⟩ := hd
+      have hm : OrderedPair x y ∈ Set.image (fun p => OrderedPair p.1 p.2) R := by
+        unfold Set.image
+        simp only [Prod.exists, Set.mem_setOf_eq]
+        exact ⟨x, ⟨y, ⟨hp, rfl⟩⟩⟩
+      unfold OrderedPair at hm
+      have : {x} ∈ ⋃₀ img := Chapter_2.exercise_2_3 {{x}, {x, y}} hm (by simp)
+      exact (Chapter_2.exercise_2_3 {x} this) (show x ∈ {x} by rfl)
+    · intro hr
+      unfold Set.Relation.ran Prod.snd at hr
+      simp only [Set.mem_image, Prod.exists, exists_eq_right] at hr
+      have ⟨t, ht⟩ := hr
+      have hm : OrderedPair t x ∈ Set.image (fun p => OrderedPair p.1 p.2) R := by
+        simp only [Set.mem_image, Prod.exists]
+        exact ⟨t, ⟨x, ⟨ht, rfl⟩⟩⟩
+      unfold OrderedPair at hm
+      have : {t, x} ∈ ⋃₀ img := Chapter_2.exercise_2_3 {{t}, {t, x}} hm
+        (show {t, x} ∈ {{t}, {t, x}} by simp)
+      exact Chapter_2.exercise_2_3 {t, x} this (show x ∈ {t, x} by simp)
+
+  · show ∀ t, t ∈ ⋃₀ ⋃₀ img → t ∈ Set.Relation.fld R
+    intro t ht
+    have ⟨T, hT⟩ : ∃ T ∈ ⋃₀ img, t ∈ T := ht
+    have ⟨T', hT'⟩ : ∃ T' ∈ img, T ∈ T' := hT.left
+    dsimp only at hT'
+    unfold Set.Relation.toOrderedPairs at hT'
+    simp only [Set.mem_image, Prod.exists] at hT'
+    have ⟨x, ⟨y, ⟨p, hp⟩⟩⟩ := hT'.left
+    have hr := hT'.right
+    rw [← hp] at hr
+    unfold OrderedPair at hr
+    simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at hr
+
+    -- Use `exercise_6_6` to prove that if `t = x` then `t ∈ dom R` and if
+    -- `t = y` then `t ∈ ran R`.
+    have hxy_mem : t = x ∨ t = y → t ∈ Set.Relation.fld R := by
+      intro ht
+      have hz : R ⊆ Set.prod (dom R) (ran R) := exercise_3_6
+      have : (x, y) ∈ Set.prod (dom R) (ran R) := hz p
+      unfold Set.prod at this
+      simp at this
+      apply Or.elim ht
+      · intro ht'
+        rw [← ht'] at this
+        exact Or.inl this.left
+      · intro ht'
+        rw [← ht'] at this
+        exact Or.inr this.right
+
+    -- Eliminate `T = {x} ∨ T = {x, y}`.
+    apply Or.elim hr
+    · intro hx
+      have := hT.right
+      rw [hx] at this
+      simp only [Set.mem_singleton_iff] at this
+      exact hxy_mem (Or.inl this)
+    · intro hxy
+      have := hT.right
+      rw [hxy] at this
+      simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at this
+      exact hxy_mem this
+
+/-- #### Exercise 3.8 (i)
+
+Show that for any set `𝓐`:
+```
+dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
+```
+-/
+theorem exercise_3_8_i {A : Set (Set.HRelation α β)}
+  : dom (⋃₀ A) = ⋃₀ { dom R | R ∈ A } := by
+  ext x
+  unfold dom Prod.fst
+  simp only [
+    Set.mem_image,
+    Set.mem_sUnion,
+    Prod.exists,
+    exists_and_right,
+    exists_eq_right,
+    Set.mem_setOf_eq,
+    exists_exists_and_eq_and
+  ]
+  apply Iff.intro
+  · intro ⟨y, t, ht, hx⟩
+    exact ⟨t, ht, y, hx⟩
+  · intro ⟨t, ht, y, hx⟩
+    exact ⟨y, t, ht, hx⟩
+
+/-- #### Exercise 3.8 (ii)
+
+Show that for any set `𝓐`:
+```
+ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
+```
+-/
+theorem exercise_3_8_ii {A : Set (Set.HRelation α β)}
+  : ran (⋃₀ A) = ⋃₀ { ran R | R ∈ A } := by
+  ext x
+  unfold ran Prod.snd
+  simp only [
+    Set.mem_image,
+    Set.mem_sUnion,
+    Prod.exists,
+    exists_eq_right,
+    Set.mem_setOf_eq,
+    exists_exists_and_eq_and
+  ]
+  apply Iff.intro
+  · intro ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩
+    exact ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩
+  · intro ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩
+    exact ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩
+
+/-- #### Exercise 3.9 (i)
+
+Discuss the result of replacing the union operation by the intersection
+operation in the preceding problem.
+```
+dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
+```
+-/
+theorem exercise_3_9_i {A : Set (Set.HRelation α β)}
+  : dom (⋂₀ A) ⊆ ⋂₀ { dom R | R ∈ A } := by
+  show ∀ x, x ∈ dom (⋂₀ A) → x ∈ ⋂₀ { dom R | R ∈ A }
+  unfold dom Prod.fst
+  simp only [
+    Set.mem_image,
+    Set.mem_sInter,
+    Prod.exists,
+    exists_and_right,
+    exists_eq_right,
+    Set.mem_setOf_eq,
+    forall_exists_index,
+    and_imp,
+    forall_apply_eq_imp_iff₂
+  ]
+  intro _ y hy R hR
+  exact ⟨y, hy R hR⟩
+
+/-- #### Exercise 3.9 (ii)
+
+Discuss the result of replacing the union operation by the intersection
+operation in the preceding problem.
+```
+ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
+```
+-/
+theorem exercise_3_9_ii {A : Set (Set.HRelation α β)}
+  : ran (⋂₀ A) ⊆ ⋂₀ { ran R | R ∈ A } := by
+  show ∀ x, x ∈ ran (⋂₀ A) → x ∈ ⋂₀ { ran R | R ∈ A }
+  unfold ran Prod.snd
+  simp only [
+    Set.mem_image,
+    Set.mem_sInter,
+    Prod.exists,
+    exists_and_right,
+    exists_eq_right,
+    Set.mem_setOf_eq,
+    forall_exists_index,
+    and_imp,
+    forall_apply_eq_imp_iff₂
+  ]
+  intro _ y hy R hR
+  exact ⟨y, hy R hR⟩
+
 /-- #### Exercise 3.12
 
 Assume that `f` and `g` are functions and show that
@@ -2166,32 +2190,6 @@ theorem exercise_3_41_a {Q : Set.Relation (ℝ × ℝ)}
     conv => right; rw [add_comm]
     exact this
 
-end Relation
-
-/-- #### Theorem 3R
-
-Let `R` be a linear ordering on `A`.
-
-(i) There is no `x` for which `xRx`.
-(ii) For distinct `x` and `y` in `A`, either `xRy` or `yRx`.
--/
-theorem theorem_3r {R : Rel α α} (hR : IsStrictTotalOrder α R)
-  : (∀ x : α, ¬ R x x) ∧ (∀ x y : α, x ≠ y → R x y ∨ R y x) := by
-  apply And.intro
-  · exact hR.irrefl
-  · intro x y h
-    apply Or.elim (hR.trichotomous x y)
-    · intro h₁
-      left
-      exact h₁
-    · intro h₁
-      apply Or.elim h₁
-      · intro h₂
-        exact absurd h₂ h
-      · intro h₂
-        right
-        exact h₂
-
 /-- #### Exercise 3.43
 
 Assume that `R` is a linear ordering on a set `A`. Show that `R⁻¹` is also a

Bookshelf/Enderton/Set/Chapter_6.lean

@@ -36,4 +36,50 @@ theorem theorem_6a_c (A : Set α) (B : Set β) (C : Set γ)
   : ∃ H, Set.BijOn H A C := by
   exact ⟨G ∘ F, Set.BijOn.comp hG hF⟩
 
+/-- #### Exercise 6.1
+
+Show that the equation
+```
+f(m, n) = 2ᵐ(2n + 1) - 1
+```
+defines a one-to-one correspondence between `ω × ω` and `ω`.
+-/
+theorem exercise_6_1
+  : Function.Bijective (fun p : ℕ × ℕ => 2 ^ p.1 * (2 * p.2 + 1) - 1) := by
+  sorry
+
+/-- #### Exercise 6.2
+
+Show that in Fig. 32 we have:
+```
+J(m, n) = [1 + 2 + ⋯ + (m + n)] + m
+        = (1 / 2)[(m + n)² + 3m + n].
+```
+-/
+theorem exercise_6_2
+  : Function.Bijective
+      (fun p : ℕ × ℕ => (1 / 2) * ((p.1 + p.2) ^ 2 + 3 * p.1 + p.2)) := by
+  sorry
+
+/-- #### Exercise 6.3
+
+Find a one-to-one correspondence between the open unit interval `(0, 1)` and `ℝ`
+that takes rationals to rationals and irrationals to irrationals.
+-/
+theorem exercise_6_3
+  : True := by
+  sorry
+
+/-- #### Exercise 6.4
+
+Construct a one-to-one correspondence between the closed unit interval
+```
+[0, 1] = {x ∈ ℝ | 0 ≤ x ≤ 1}
+```
+and the open unit interval `(0, 1)`.
+-/
+theorem exercise_6_4
+  : ∃ F, Set.BijOn F (Set.Ioo 0 1) (@Set.univ ℝ) := by
+  sorry
+
 end Enderton.Set.Chapter_6