Enderton (set). Partially work on finite set exercises.
parent
e29795c55e
commit
edef7e9b58
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.2
|
||||
/-- #### Exercise 6.8
|
||||
|
||||
Show that in Fig. 32 we have:
|
||||
```
|
||||
J(m, n) = [1 + 2 + ⋯ + (m + n)] + m
|
||||
= (1 / 2)[(m + n)² + 3m + n].
|
||||
```
|
||||
Prove that the union 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
|
||||
theorem exercise_6_8 {A B : Set α} (hA : Set.Finite A) (hB : Set.Finite B)
|
||||
: Set.Finite (A ∪ B) := by
|
||||
sorry
|
||||
|
||||
/-- #### Exercise 6.3
|
||||
/-- #### Exercise 6.9
|
||||
|
||||
Find a one-to-one correspondence between the open unit interval `(0, 1)` and `ℝ`
|
||||
that takes rationals to rationals and irrationals to irrationals.
|
||||
Prove that the Cartesian product of two finites sets is finite, without any use
|
||||
of arithmetic.
|
||||
-/
|
||||
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
|
||||
|
|
|
|||
Loading…
Reference in New Issue