From edef7e9b58bfdccd95ffebf30b6454aebf4b0e1c Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 20 Sep 2023 13:39:59 -0600 Subject: [PATCH] Enderton (set). Partially work on finite set exercises. --- Bookshelf/Enderton/Set.tex | 97 +++++++++++++++++++++------ Bookshelf/Enderton/Set/Chapter_6.lean | 78 ++++++++++----------- 2 files changed, 117 insertions(+), 58 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index a18d105..137c4ca 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/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 diff --git a/Bookshelf/Enderton/Set/Chapter_6.lean b/Bookshelf/Enderton/Set/Chapter_6.lean index e87c4fa..685cfb2 100644 --- a/Bookshelf/Enderton/Set/Chapter_6.lean +++ b/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