Add note.

Bookshelf/Enderton/Set.tex

@@ -64,6 +64,47 @@
   A \textbf{binary operation} on a set $A$ is a \nameref{ref:function} from
     $A \times A$ into $A$.
 
+\section{\defined{Cardinal Arithmetic}}%
+\hyperlabel{sec:cardinal-arithmetic}
+
+  Let $\kappa$ and $\lambda$ be any cardinal numbers.
+  \begin{enumerate}[(a)]
+    \item $\kappa + \lambda = \card{(K \cup L)}$, where $K$ and $L$ are any
+      disjoint sets of cardinality $\kappa$ and $\lambda$, respectively.
+    \item $\kappa \cdot \lambda = \card{(K \times L)}$, where $K$ and $L$ are
+      any sets of cardinality $\kappa$ and $\lambda$, respectively.
+    \item $\kappa^\lambda = \card{(^L{K})}$, where $K$ and $L$ are any sets of
+      cardinality $\kappa$ and $\lambda$, respectively.
+  \end{enumerate}
+
+  \lean{Mathlib/SetTheory/Cardinal/Basic}
+    {Cardinal.add\_def}
+
+  \lean{Mathlib/SetTheory/Cardinal/Basic}
+    {Cardinal.mul\_def}
+
+  \lean{Mathlib/SetTheory/Cardinal/Basic}
+    {Cardinal.power\_def}
+
+\section{\defined{Cardinal Number}}%
+\hyperlabel{ref:cardinal-number}
+
+  For any set $C$, the \textbf{cardinal number} of set $C$ is denoted as
+    $\card{C}$.
+  Furthermore,
+    \begin{enumerate}[(a)]
+      \item For any sets $A$ and $B$,
+        $$\card{A} = \card{B} \quad\text{iff}\quad \equinumerous{A}{B}.$$
+      \item For a finite set $A$, $\card{A}$ is the \nameref{ref:natural-number}
+        $n$ for which $\equinumerous{A}{n}$.
+    \end{enumerate}
+
+  \lean{Mathlib/Data/Finset/Card}
+    {Finset.card}
+
+  \lean{Mathlib/SetTheory/Cardinal/Basic}
+    {Cardinal}
+
 \section{\defined{Cartesian Product}}%
 \hyperlabel{ref:cartesian-product}
 
@@ -77,19 +118,6 @@
 
   \lean{Mathlib/Data/Set/Prod}{Set.prod}
 
-\section{\defined{Cardinal Arithmetic}}%
-\hyperlabel{sec:cardinal-arithmetic}
-
-  Let $\kappa$ and $\lambda$ be any cardinal numbers.
-  \begin{enumerate}[(a)]
-    \item $\kappa + \lambda = \card{(K \cup L)}$, where $K$ and $L$ are any
-      disjoint sets of cardinality $\kappa$ and $\lambda$, respectively.
-    \item $\kappa \cdot \lambda = \card{(K \times L)}$, where $K$ and $L$ are
-      any sets of cardinality $\kappa$ and $\lambda$, respectively.
-    \item $\kappa^\lambda = \card{^L{K}}$, where $K$ and $L$ are any sets of
-      cardinality $\kappa$ and $\lambda$, respectively.
-  \end{enumerate}
-
 \section{\defined{Compatible}}%
 \hyperlabel{ref:compatible}
 
@@ -1876,7 +1904,7 @@
     We proceed by contradiction.
     Suppose there existed a set $A$ consisting of every singleton.
     Then the \nameref{ref:union-axiom} suggests $\bigcup A$ is a set.
-    But this set is precisely the class of all sets, which is \textit{not} a
+    But this "set" is precisely the class of all sets, which is \textit{not} a
       set.
     Thus our original assumption was incorrect.
     That is, there is no set to which every singleton belongs.
@@ -9530,7 +9558,7 @@
     Refer to \nameref{sub:theorem-6a}.
   \end{proof}
 
-\subsection{\sorry{Exercise 6.6}}%
+\subsection{\unverified{Exercise 6.6}}%
 \hyperlabel{sub:exercise-6.6}
 
   Let $\kappa$ be a nonzero cardinal number.
@@ -9538,20 +9566,49 @@
     belongs.
 
   \begin{proof}
-    TODO
+    Let $\kappa$ be a nonzero cardinal number and define
+      $$\mathbf{K}_\kappa = \{ X \mid \card{X} = \kappa \}.$$
+    For the sake of contradiction, suppose $\mathbf{K}_\kappa$ is a set.
+    Then the \nameref{ref:union-axiom} suggests $\bigcup \mathbf{K}_{\kappa}$ is
+      a set.
+    But this "set" is precisely the class of all sets, which is \textit{not} a
+      set.
+    Thus our original assumption was incorrect.
+    That is, there does not exist a set to which every set of cardinality
+      $\kappa$ belongs.
   \end{proof}
 
-\subsection{\sorry{Exercise 6.7}}%
+\subsection{\pending{Exercise 6.7}}%
 \hyperlabel{sub:exercise-6.7}
 
   Assume that $A$ is finite and $f \colon A \rightarrow A$.
   Show that $f$ is one-to-one iff $\ran{f} = A$.
 
+  \code*{Bookshelf/Enderton/Set/Chapter\_6}
+    {Enderton.Set.Chapter\_6.exercise\_6\_7}
+
   \begin{proof}
-    TODO
+    Let $A$ be a \nameref{ref:finite-set} and $f \colon A \rightarrow A$.
+
+    \paragraph{($\Rightarrow$)}%
+
+      Suppose $f$ is one-to-one.
+      Then $f$ is a one-to-one correspondence between $A$ and $\ran{f}$.
+      That is, $\equinumerous{A}{\ran{f}}$.
+      Because $f$ maps $A$ onto $A$, $\ran{f} \subseteq A$.
+      Hence $\ran{f} \subset A$ or $\ran{f} = A$.
+      But, by \nameref{sub:corollary-6c}, $\ran{f}$ cannot be a proper subset of
+        $A$.
+      Thus $\ran{f} = A$.
+
+    \paragraph{($\Leftarrow$)}%
+
+      Suppose $\ran{f} = A$.
+      TODO: by induction?
+
   \end{proof}
 
-\subsection{\sorry{Exercise 6.8}}%
+\subsection{\pending{Exercise 6.8}}%
 \hyperlabel{sub:exercise-6.8}
 
   Prove that the union of two finite sets is finite, without any use of
@@ -9561,7 +9618,7 @@
     TODO
   \end{proof}
 
-\subsection{\sorry{Exercise 6.9}}%
+\subsection{\pending{Exercise 6.9}}%
 \hyperlabel{sub:exercise-6.9}
 
   Prove that the Cartesian product of two finite sets is finite, without any use

Bookshelf/Enderton/Set/Chapter_6.lean

@@ -675,50 +675,52 @@ theorem corollary_6g {S S' : Set α} (hS : Set.Finite S) (hS' : S' ⊆ S)
   · intro h
     rwa [h]
 
-/-- #### Exercise 6.1
+/-- #### Exercise 6.7
 
-Show that the equation
-```
-f(m, n) = 2ᵐ(2n + 1) - 1
-```
-defines a one-to-one correspondence between `ω × ω` and `ω`.
+Assume that `A` is finite and `f : A → A`. Show that `f` is one-to-one **iff**
+`ran f = A`.
 -/
-theorem exercise_6_1
-  : Function.Bijective (fun p : ℕ × ℕ => 2 ^ p.1 * (2 * p.2 + 1) - 1) := by
+theorem exercise_6_7 [DecidableEq α] [Nonempty α] {A : Set α} {f : α → α}
+  (hA₁ : Set.Finite A) (hA₂ : Set.MapsTo f A A)
+  : Set.InjOn f A ↔ f '' A = A := by
+  apply Iff.intro
+  · intro hf
+    have hf₂ : A ≈ f '' A := by
+      refine ⟨f, ?_, hf, ?_⟩
+      · -- `Set.MapsTo f A (f '' A)`
+        intro x hx
+        simp only [Set.mem_image]
+        exact ⟨x, hx, rfl⟩
+      · -- `Set.SurjOn f A (f '' A)`
+        intro _ hx
+        exact hx
+    have hf₃ : f '' A  ⊆ A := by
+      show ∀ x, x ∈ f '' A → x ∈ A
+      intro x ⟨a, ha₁, ha₂⟩
+      rw [← ha₂]
+      exact hA₂ ha₁
+    rw [subset_iff_ssubset_or_eq] at hf₃
+    exact Or.elim hf₃ (fun h => absurd hf₂ (corollary_6c hA₁ h)) id
+  · intro hf₁
+    sorry
+
+/-- #### Exercise 6.8
+
+Prove that the union of two finites sets is finite, without any use of
+arithmetic.
+-/
+theorem exercise_6_8 {A B : Set α} (hA : Set.Finite A) (hB : Set.Finite B)
+  : Set.Finite (A ∪ B) := by
   sorry
 
-/-- #### Exercise 6.2
+/-- #### Exercise 6.9
 
-Show that in Fig. 32 we have:
-```
-J(m, n) = [1 + 2 + ⋯ + (m + n)] + m
-        = (1 / 2)[(m + n)² + 3m + n].
-```
+Prove that the Cartesian product of two finites sets is finite, without any use
+of arithmetic.
 -/
-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
+theorem exercise_6_9 {A : Set α} {B : Set β}
+  (hA : Set.Finite A) (hB : Set.Finite B)
+  : Set.Finite (Set.prod A B) := by
   sorry
 
 end Enderton.Set.Chapter_6