Enderton (set). Add Lean scaffolding for finite set theorems/bijections.

finite-set-exercises
Joshua Potter 2023-08-24 07:50:47 -06:00
parent a00a5f5523
commit 3bf6f13055
2 changed files with 39 additions and 6 deletions

View File

@ -3171,8 +3171,8 @@
\end{proof}
\subsection{\unverified{Bijections are Two-Sided Inverses}}%
\hyperlabel{sub:bijections-two-sided-inverses}
\subsection{\unverified{Bijections and Inverses}}%
\hyperlabel{sub:bijections-inverses}
\begin{corollary}
A function $f$ is a one-to-one correspondence if and only if it has a left
@ -3188,6 +3188,30 @@
inverse.
\end{proof}
\subsection{\unverified{Left and Right Inverses and Two-Sided Inverses}}%
\hyperlabel{sub:left-right-inverse-two-sided-inverse}
\begin{lemma}
Let $f$ be a function with left inverse $g_1$ and right inverse $g_2$.
Then $g_1 = g_2 = f^{-1}$.
\end{lemma}
\begin{proof}
Let $I$ denote the identity map with appropriate domain and codomain
depending on placement in the following:
\begin{align*}
g_1
& = g_1 \circ I \\
& = g_1 \circ (f \circ g_2) \\
& = (g_1 \circ f) \circ g_2 \\
& = I \circ g_2 \\
& = g_2.
\end{align*}
By \nameref{sub:bijections-inverses}, $f$ is a bijection meaning $f^{-1}$
is both a left and right inverse.
Hence $g_1 = g_2 = f^{-1}$.
\end{proof}
\subsection{\verified{Theorem 3K(a)}}%
\hyperlabel{sub:theorem-3k-a}

View File

@ -67,6 +67,11 @@ No natural number is equinumerous to a proper subset of itself.
-/
theorem pigeonhole_principle (m n : ) (hm : m < n)
: ∀ f : Fin m → Fin n, ¬ Function.Bijective f := by
induction n with
| zero =>
intro f hf
simp at hm
| succ n ih =>
sorry
/-- #### Corollary 6C
@ -97,8 +102,8 @@ theorem corollary_6d_b
Any finite set is equinumerous to a unique natural number.
-/
theorem corollary_6e (S : Set α) (f : S → Fin n) (hf : Function.Bijective f)
: S ≃ Fin m → m = n := by
theorem corollary_6e (S : Set α) (hn : S ≃ Fin n) (hm : S ≃ Fin m)
: m = n := by
sorry
/-- #### Lemma 6F
@ -106,10 +111,14 @@ theorem corollary_6e (S : Set α) (f : S → Fin n) (hf : Function.Bijective f)
If `C` is a proper subset of a natural number `n`, then `C ≈ m` for some `m`
less than `n`.
-/
lemma lemma_6f {n : } (C S : Finset ) (hC : C ⊂ S) (hS : S ≃ Fin n)
lemma lemma_6f {n : } (hC : C ⊂ Finset.range n)
: ∃ m : , m < n ∧ ∃ f : C → Fin m, Function.Bijective f := by
sorry
theorem corollary_6g (S S' : Set α) (hS : Finite S) (hS' : S' ⊆ S)
: Finite S' := by
sorry
/-- #### Exercise 6.1
Show that the equation