Compare commits

...

3 Commits

Author SHA1 Message Date
Joshua Potter 0a3b8f082b Add note. 2023-09-21 06:15:17 -06:00
Joshua Potter a8520e74bd More progress. 2023-09-20 17:49:03 -06:00
Joshua Potter a368f32558 Finite set exercises. 2023-09-20 13:39:59 -06:00
2 changed files with 117 additions and 58 deletions

View File

@ -64,6 +64,47 @@
A \textbf{binary operation} on a set $A$ is a \nameref{ref:function} from A \textbf{binary operation} on a set $A$ is a \nameref{ref:function} from
$A \times A$ into $A$. $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}}% \section{\defined{Cartesian Product}}%
\hyperlabel{ref:cartesian-product} \hyperlabel{ref:cartesian-product}
@ -77,19 +118,6 @@
\lean{Mathlib/Data/Set/Prod}{Set.prod} \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}}% \section{\defined{Compatible}}%
\hyperlabel{ref:compatible} \hyperlabel{ref:compatible}
@ -1876,7 +1904,7 @@
We proceed by contradiction. We proceed by contradiction.
Suppose there existed a set $A$ consisting of every singleton. Suppose there existed a set $A$ consisting of every singleton.
Then the \nameref{ref:union-axiom} suggests $\bigcup A$ is a set. 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. set.
Thus our original assumption was incorrect. Thus our original assumption was incorrect.
That is, there is no set to which every singleton belongs. That is, there is no set to which every singleton belongs.
@ -9530,7 +9558,7 @@
Refer to \nameref{sub:theorem-6a}. Refer to \nameref{sub:theorem-6a}.
\end{proof} \end{proof}
\subsection{\sorry{Exercise 6.6}}% \subsection{\unverified{Exercise 6.6}}%
\hyperlabel{sub:exercise-6.6} \hyperlabel{sub:exercise-6.6}
Let $\kappa$ be a nonzero cardinal number. Let $\kappa$ be a nonzero cardinal number.
@ -9538,20 +9566,49 @@
belongs. belongs.
\begin{proof} \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} \end{proof}
\subsection{\sorry{Exercise 6.7}}% \subsection{\pending{Exercise 6.7}}%
\hyperlabel{sub:exercise-6.7} \hyperlabel{sub:exercise-6.7}
Assume that $A$ is finite and $f \colon A \rightarrow A$. Assume that $A$ is finite and $f \colon A \rightarrow A$.
Show that $f$ is one-to-one iff $\ran{f} = 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} \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} \end{proof}
\subsection{\sorry{Exercise 6.8}}% \subsection{\pending{Exercise 6.8}}%
\hyperlabel{sub:exercise-6.8} \hyperlabel{sub:exercise-6.8}
Prove that the union of two finite sets is finite, without any use of Prove that the union of two finite sets is finite, without any use of
@ -9561,7 +9618,7 @@
TODO TODO
\end{proof} \end{proof}
\subsection{\sorry{Exercise 6.9}}% \subsection{\pending{Exercise 6.9}}%
\hyperlabel{sub:exercise-6.9} \hyperlabel{sub:exercise-6.9}
Prove that the Cartesian product of two finite sets is finite, without any use Prove that the Cartesian product of two finite sets is finite, without any use

View File

@ -675,50 +675,52 @@ theorem corollary_6g {S S' : Set α} (hS : Set.Finite S) (hS' : S' ⊆ S)
· intro h · intro h
rwa [h] rwa [h]
/-- #### Exercise 6.1 /-- #### Exercise 6.7
Show that the equation Assume that `A` is finite and `f : A → A`. Show that `f` is one-to-one **iff**
``` `ran f = A`.
f(m, n) = 2ᵐ(2n + 1) - 1
```
defines a one-to-one correspondence between `ω × ω` and `ω`.
-/ -/
theorem exercise_6_1 theorem exercise_6_7 [DecidableEq α] [Nonempty α] {A : Set α} {f : αα}
: Function.Bijective (fun p : × => 2 ^ p.1 * (2 * p.2 + 1) - 1) := by (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 sorry
/-- #### Exercise 6.2 /-- #### Exercise 6.8
Show that in Fig. 32 we have: Prove that the union of two finites sets is finite, without any use of
``` arithmetic.
J(m, n) = [1 + 2 + ⋯ + (m + n)] + m
= (1 / 2)[(m + n)² + 3m + n].
```
-/ -/
theorem exercise_6_2 theorem exercise_6_8 {A B : Set α} (hA : Set.Finite A) (hB : Set.Finite B)
: Function.Bijective : Set.Finite (A B) := by
(fun p : × => (1 / 2) * ((p.1 + p.2) ^ 2 + 3 * p.1 + p.2)) := by
sorry sorry
/-- #### Exercise 6.3 /-- #### Exercise 6.9
Find a one-to-one correspondence between the open unit interval `(0, 1)` and `` Prove that the Cartesian product of two finites sets is finite, without any use
that takes rationals to rationals and irrationals to irrationals. of arithmetic.
-/ -/
theorem exercise_6_3 theorem exercise_6_9 {A : Set α} {B : Set β}
: True := by (hA : Set.Finite A) (hB : Set.Finite B)
sorry : Set.Finite (Set.prod A B) := by
/-- #### 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 sorry
end Enderton.Set.Chapter_6 end Enderton.Set.Chapter_6