diff --git a/Bookshelf/Enderton/Set.lean b/Bookshelf/Enderton/Set.lean index 3a0abbd..0aaae73 100644 --- a/Bookshelf/Enderton/Set.lean +++ b/Bookshelf/Enderton/Set.lean @@ -2,5 +2,6 @@ import Bookshelf.Enderton.Set.Chapter_1 import Bookshelf.Enderton.Set.Chapter_2 import Bookshelf.Enderton.Set.Chapter_3 import Bookshelf.Enderton.Set.Chapter_4 +import Bookshelf.Enderton.Set.Chapter_6 import Bookshelf.Enderton.Set.OrderedPair import Bookshelf.Enderton.Set.Relation \ No newline at end of file diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 170ae80..65b27ea 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -127,8 +127,8 @@ \section{\defined{Equinumerous}}% \hyperlabel{ref:equinumerous} -A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and - only if there is a one-to-one \nameref{ref:function} from $A$ onto $B$. +A set $A$ is \textbf{equinumerous} to a set $B$ (written $\equinumerous{A}{B}$) + if and only if there is a one-to-one \nameref{ref:function} from $A$ onto $B$. \lean*{Mathlib/Init/Function} {Function.Bijective} @@ -215,14 +215,26 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and only one $x$ such that $xFy$. One-to-one functions are sometimes called \textbf{injections}. - \lean*{Mathlib/Init/Function} - {Function.Injective} + \code*{Bookshelf/Enderton/Set/Relation} + {Set.Relation.isSingleValued} - \lean{Mathlib/Init/Function} - {Function.Surjective} + \code{Bookshelf/Enderton/Set/Relation} + {Set.Relation.isSingleRooted} - \lean{Mathlib/Init/Function} - {Function.Bijective} + \code{Bookshelf/Enderton/Set/Relation} + {Set.Relation.isOneToOne} + + \lean{Mathlib/Data/Set/Function} + {Set.MapsTo} + + \lean{Mathlib/Data/Set/Function} + {Set.InjOn} + + \lean{Mathlib/Data/Set/Function} + {Set.SurjOn} + + \lean{Mathlib/Data/Set/Function} + {Set.BijOn} \section{\defined{Image}}% \hyperlabel{ref:image} @@ -2863,11 +2875,10 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and \end{proof} -\subsection{\verified{Lemma 1}}% -\hyperlabel{sub:lemma-1} +\subsection{\verified{One-to-One Inverse}}% \hyperlabel{sub:one-to-one-inverse} - \begin{lemma}[1] + \begin{lemma} For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \end{lemma} @@ -2992,6 +3003,43 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and \end{proof} +\subsection{\verified{One-to-One Composition}}% +\hyperlabel{sub:one-to-one-composition} + + \begin{lemma} + Let $F$ and $G$ be one-to-one functions. + Then $F \circ G$ is one-to-one as well. + \end{lemma} + + \code{Bookshelf/Enderton/Set/Relation} + {Set.Relation.one\_to\_one\_comp\_is\_one\_to\_one} + + \begin{proof} + Let $F \colon B \rightarrow C$ and $G \colon A \rightarrow B$ be + one-to-one \nameref{ref:function}s from sets $A$, $B$, and $C$. + By definition of the \nameref{ref:composition} of functions, + \begin{equation} + \hyperlabel{sub:one-to-one-composition-eq1} + F \circ G = \{\tuple{u, v} \mid \exists t(uGt \land tFv)\}. + \end{equation} + By \nameref{sub:theorem-3h}, $F \circ G$ is a function. + All that remains is proving $F \circ G$ is single-valued, i.e. for each + $y \in \ran{F \circ G}$, there is only one $x$ such that + $\tuple{x, y} \in F \circ G$. + + To that end let $y \in \ran{(F \circ G)}$. + Then there exists some $x_1 \in \dom{(F \circ G)}$ such that + $\tuple{x_1, y} \in F \circ G$. + Suppose there also exists some $x_2 \in \dom{(F \circ G)}$ such that + $\tuple{x_2, y} \in F \circ G$. + By \eqref{sub:one-to-one-composition-eq1}, there exists a $t_1$ such that + $x_1Gt_1$ and $t_1Fy$. + Likewise, there exists some $t_2$ such that $x_2Gt_2$ and $t_2Fy$. + But $F$ is one-to-one meaning $t_1 = t_2$. + Similarly, $G$ is one-to-one meaning $x_1 = x_2$. + Hence $F \circ G$ is single-valued. + \end{proof} + \subsection{\verified{Theorem 3I}}% \hyperlabel{sub:theorem-3i} @@ -6232,11 +6280,10 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and \end{proof} -\subsection{\verified{Lemma 2}}% -\hyperlabel{sub:lemma-2} -\hyperlabel{sub:succ-add-eq-add-succ} +\subsection{\verified{Successor Commutativity}}% +\hyperlabel{sub:successor-commutativity} - \begin{lemma}[2] + \begin{lemma} For all $m, n \in \omega$, $A_{m^+}(n) = A_m(n^+)$. In other words, $$m^+ + n = m + n^+.$$ \end{lemma} @@ -6314,13 +6361,13 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and Then \begin{align*} m^+ + (n + p) - & = m + (n + p)^+ & \textref{sub:succ-add-eq-add-succ} \\ + & = m + (n + p)^+ & \textref{sub:successor-commutativity} \\ & = (m + (n + p))^+ & \textref{sub:theorem-4i} \\ & = ((m + n) + p)^+ & \eqref{sub:theorem-4k-1-eq1} \\ & = (m + n) + p^+ & \textref{sub:theorem-4i} \\ - & = (m + n)^+ + p & \textref{sub:succ-add-eq-add-succ} \\ + & = (m + n)^+ + p & \textref{sub:successor-commutativity} \\ & = (m + n^+) + p & \textref{sub:theorem-4i} \\ - & = (m^+ + n) + p. & \textref{sub:succ-add-eq-add-succ} + & = (m^+ + n) + p. & \textref{sub:successor-commutativity} \end{align*} Thus $m^+ \in S$. @@ -6371,7 +6418,7 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and Then \begin{align*} m^+ + n - & = m + n^+ & \textref{sub:succ-add-eq-add-succ} \\ + & = m + n^+ & \textref{sub:successor-commutativity} \\ & = (m + n)^+ & \textref{sub:theorem-4i} \\ & = (n + m)^+ & \eqref{sub:theorem-4k-2-eq1} \\ & = n + m^+. & \textref{sub:theorem-4i} @@ -6479,7 +6526,7 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and & = m^+ \cdot n + m^+ & \textref{sub:theorem-4j} \\ & = (m \cdot n + n) + m^+ & \eqref{sub:successor-distribution-eq1} \\ & = m \cdot n + (n + m^+) & \textref{sub:theorem-4k-1} \\ - & = m \cdot n + (n^+ + m) & \textref{sub:succ-add-eq-add-succ} \\ + & = m \cdot n + (n^+ + m) & \textref{sub:successor-commutativity} \\ & = m \cdot n + (m + n^+) & \textref{sub:theorem-4k-2} \\ & = (m \cdot n + m) + n^+ & \textref{sub:theorem-4k-1} \\ & = m \cdot n^+ + n^+. & \textref{sub:theorem-4j} @@ -6597,7 +6644,7 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and Then \begin{align*} m^+ + 1 - & = m + 1^+ & \textref{sub:succ-add-eq-add-succ} \\ + & = m + 1^+ & \textref{sub:successor-commutativity} \\ & = (m + 1)^+ & \textref{sub:theorem-4i} \\ & = (m^+)^+. & \eqref{sub:successor-identity-eq1} \end{align*} @@ -8395,20 +8442,55 @@ A set $A$ is \textbf{equinumerous} to a set $B$ (written $A \approx B$) if and \section{Equinumerosity}% \hyperlabel{sec:equinumerosity} -\subsection{\sorry{Theorem 6A}}% +\subsection{\verified{Theorem 6A}}% \hyperlabel{sub:theorem-6a} \begin{theorem}[6A] For any sets $A$, $B$, and $C$, \begin{enumerate}[(a)] - \item $A \approx A$. - \item If $A \approx B$, then $B \approx A$. - \item If $A \approx B$ and $B \approx C$, then $A \approx C$. + \item $\equinumerous{A}{A}$. + \item If $\equinumerous{A}{B}$, then $\equinumerous{B}{A}$. + \item If $\equinumerous{A}{B}$ and $\equinumerous{B}{C}$, then + $\equinumerous{A}{C}$. \end{enumerate} \end{theorem} + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.theorem\_6a\_a} + + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.theorem\_6a\_b} + + \code{Bookshelf/Enderton/Set/Chapter\_6} + {Enderton.Set.Chapter\_6.theorem\_6a\_c} + \begin{proof} - TODO + + Let $A$, $B$, and $C$ be arbitrary sets. + + \paragraph{(a)}% + + Consider function $I_A \colon A \rightarrow A$ given by $I_A(x) = x$. + This function is trivially a bijection between $A$ and $A$. + Thus $A$ is \nameref{ref:equinumerous} to $A$. + + \paragraph{(b)}% + + Suppose $\equinumerous{A}{B}$. + Then there exists a one-to-one function $f \colon A \rightarrow B$. + By \nameref{sub:one-to-one-inverse}, $f^{-1} \colon B \rightarrow A$ + is also one-to-one. + Thus $\equinumerous{B}{A}$. + + \paragraph{(c)}% + + Suppose $\equinumerous{A}{B}$ and $\equinumerous{B}{C}$. + Then there exist one-to-one functions $f \colon A \rightarrow B$ and + $g \colon B \rightarrow C$. + Then, by \nameref{sub:one-to-one-composition}, + $g \circ f \colon A \rightarrow C$ is one-to-one. + Thus $\equinumerous{A}{C}$. + \end{proof} \subsection{\sorry{Theorem 6B}}% diff --git a/Bookshelf/Enderton/Set/Chapter_6.lean b/Bookshelf/Enderton/Set/Chapter_6.lean new file mode 100644 index 0000000..9ea90c4 --- /dev/null +++ b/Bookshelf/Enderton/Set/Chapter_6.lean @@ -0,0 +1,39 @@ +import Mathlib.Data.Set.Function +import Mathlib.Data.Rel + +/-! # Enderton.Set.Chapter_6 + +Cardinal Numbers and the Axiom of Choice +-/ + +namespace Enderton.Set.Chapter_6 + +/-! #### Theorem 6A + +For any sets `A`, `B`, and `C`, + +(a) `A ≈ A`. +(b) If `A ≈ B`, then `B ≈ A`. +(c) If `A ≈ B` and `B ≈ C`, then `A ≈ C`. +-/ + +theorem theorem_6a_a (A : Set α) + : ∃ f, Set.BijOn f A A := by + refine ⟨fun x => x, ?_⟩ + unfold Set.BijOn Set.MapsTo Set.InjOn Set.SurjOn + simp only [imp_self, implies_true, Set.image_id', true_and] + exact Eq.subset rfl + +theorem theorem_6a_b [Nonempty α] (A : Set α) (B : Set β) + (f : α → β) (hf : Set.BijOn f A B) + : ∃ g, Set.BijOn g B A := by + refine ⟨Function.invFunOn f A, ?_⟩ + exact (Set.bijOn_comm $ Set.BijOn.invOn_invFunOn hf).mpr hf + +theorem theorem_6a_c (A : Set α) (B : Set β) (C : Set γ) + (f : α → β) (hf : Set.BijOn f A B) + (g : β → γ) (hg : Set.BijOn g B C) + : ∃ h, Set.BijOn h A C := by + exact ⟨g ∘ f, Set.BijOn.comp hg hf⟩ + +end Enderton.Set.Chapter_6 diff --git a/Bookshelf/Enderton/Set/Relation.lean b/Bookshelf/Enderton/Set/Relation.lean index e4eee6e..75df110 100644 --- a/Bookshelf/Enderton/Set/Relation.lean +++ b/Bookshelf/Enderton/Set/Relation.lean @@ -440,6 +440,26 @@ theorem single_valued_comp_is_single_valued have hk₂ := hy'.right y₁ (mem_pair_imp_snd_mem_ran ht₂.right) ht₂.right rw [hk₁, hk₂] +/-- +The composition of two one-to-one `Relation`s is one-to-one. +-/ +theorem one_to_one_comp_is_one_to_one + {F : HRelation β γ} {G : HRelation α β} + (hF : isOneToOne F) (hG : isOneToOne G) + : isOneToOne (comp F G) := by + refine ⟨single_valued_comp_is_single_valued hF.left hG.left, ?_⟩ + intro y hy + unfold ExistsUnique + have ⟨x₁, hx₁⟩ := ran_exists hy + refine ⟨x₁, ⟨mem_pair_imp_fst_mem_dom hx₁, hx₁⟩, ?_⟩ + intro x₂ ⟨_, hx₂⟩ + have ⟨t₁, ht₁⟩ := hx₁ + have ⟨t₂, ht₂⟩ := hx₂ + simp only at ht₁ ht₂ + have ht : t₁ = t₂ := single_rooted_eq_unique hF.right ht₁.right ht₂.right + rw [ht] at ht₁ + exact single_rooted_eq_unique hG.right ht₂.left ht₁.left + /-- For `Relation`s `F` and `G`, `(F ∘ G)⁻¹ = G⁻¹ ∘ F⁻¹`. -/ diff --git a/preamble.tex b/preamble.tex index 2709b62..249ba19 100644 --- a/preamble.tex +++ b/preamble.tex @@ -168,6 +168,7 @@ \newcommand{\ceil}[1]{\left\lceil#1\right\rceil} \newcommand{\ctuple}[2]{\left< #1, \cdots, #2 \right>} \newcommand{\dom}[1]{\textop{dom}{#1}} +\newcommand{\equinumerous}[2]{#1 \approx #2} \newcommand{\fld}[1]{\textop{fld}{#1}} \newcommand{\floor}[1]{\left\lfloor#1\right\rfloor} \newcommand{\icc}[2]{\left[#1, #2\right]} @@ -180,7 +181,6 @@ \newcommand{\ran}[1]{\textop{ran}{#1}} \newcommand{\textop}[1]{\mathop{\text{#1}}} \newcommand{\tuple}[1]{\left< #1 \right>} - \newcommand{\ubar}[1]{\text{\b{$#1$}}} \let\oldemptyset\emptyset