Enderton (set). Begin adding Chapter 6 lean theorems.

Bookshelf/Enderton/Set.tex

@@ -150,6 +150,9 @@
   \lean*{Mathlib/Init/Function}
     {Function.Bijective}
 
+  \lean{Mathlib/Logic/Equiv/Defs}
+    {Equiv}
+
 \section{\defined{Equivalence Class}}%
 \hyperlabel{ref:equivalence-class}
 
@@ -214,8 +217,8 @@
   A set is \textbf{finite} if and only if it is \nameref{ref:equinumerous} to a
     \nameref{ref:natural-number}.
 
-  \lean{Mathlib/Data/Finset/Basic}
+  \lean*{Mathlib/Data/Set/Finite}
-    {Finset}
+    {Set.Finite}
 
 \section{\defined{Function}}%
 \hyperlabel{ref:function}
@@ -298,6 +301,9 @@
   A set is \textbf{infinite} if and only if it is not a
     \nameref{ref:finite-set}.
 
+  \lean*{Mathlib/Data/Set/Finite}
+    {Set.Infinite}
+
 \section{\defined{Infinity Axiom}}%
 \hyperlabel{ref:infinity-axiom}
 
@@ -3159,6 +3165,23 @@
 
   \end{proof}
 
+\subsection{\unverified{Bijections are Two-Sided Inverses}}%
+\hyperlabel{sub:bijections-two-sided-inverses}
+
+  \begin{corollary}
+    A function $f$ is a one-to-one correspondence if and only if it has a left
+      and right inverse.
+  \end{corollary}
+
+  \begin{proof}
+    By definition, a one-to-one correspondence $f$ between sets $A$ and $B$ must
+      be both one-to-one and onto.
+    By \nameref{sub:theorem-3j}, $f$ is one-to-one if and only if it has a left
+      inverse.
+    The same theorem states that $f$ is onto $B$ if and only if it has a right
+      inverse.
+  \end{proof}
+
 \subsection{\verified{Theorem 3K(a)}}%
 \hyperlabel{sub:theorem-3k-a}
 
@@ -8520,13 +8543,16 @@
 
   \end{proof}
 
-\subsection{\pending{Theorem 6B}}%
+\subsection{\verified{Theorem 6B}}%
 \hyperlabel{sub:theorem-6b}
 
   \begin{theorem}[6B]
     No set is \nameref{ref:equinumerous} to its powerset.
   \end{theorem}
 
+  \code*{Bookshelf/Enderton/Set/Chapter\_6}
+    {Enderton.Set.Chapter\_6.theorem\_6b}
+
   \begin{proof}
     Let $A$ be an arbitrary set and $f \colon A \rightarrow \powerset{A}$.
     Define $\phi = \{a \in A \mid a \not\in f(a)\}$.

Bookshelf/Enderton/Set/Chapter_6.lean

@@ -1,3 +1,5 @@
+import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Set.Finite
 import Mathlib.Data.Set.Function
 import Mathlib.Data.Rel
 
@@ -36,6 +38,78 @@ theorem theorem_6a_c (A : Set α) (B : Set β) (C : Set γ)
   : ∃ H, Set.BijOn H A C := by
   exact ⟨G ∘ F, Set.BijOn.comp hG hF⟩
 
+/-- #### Theorem 6B
+
+No set is equinumerous to its powerset.
+-/
+theorem theorem_6b (A : Set α)
+  : ∀ f, ¬ Set.BijOn f A (𝒫 A) := by
+  intro f hf
+  unfold Set.BijOn at hf
+  let φ := { a ∈ A | a ∉ f a }
+  suffices ∀ a ∈ A, f a ≠ φ by
+    have hφ := hf.right.right (show φ ∈ 𝒫 A by simp)
+    have ⟨a, ha⟩ := hφ
+    exact absurd ha.right (this a ha.left)
+  intro a ha hfa
+  by_cases h : a ∈ f a
+  · have h' := h
+    rw [hfa] at h
+    simp only [Set.mem_setOf_eq] at h
+    exact absurd h' h.right
+  · rw [Set.Subset.antisymm_iff] at hfa
+    have := hfa.right ⟨ha, h⟩
+    exact absurd this h
+
+/-- #### Pigeonhole Principle
+
+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
+  sorry
+
+/-- #### Corollary 6C
+
+No finite set is equinumerous to a proper subset of itself.
+-/
+theorem corollary_6c (S S' : Finset α) (hS : S' ⊂ S)
+  : ∀ f : S → S', ¬ Function.Bijective f := by
+  sorry
+
+/-- #### Corollary 6D (a)
+
+Any set equinumerous to a proper subset of itself is infinite.
+-/
+theorem corollary_6d_a (S S' : Set α) (hS : S' ⊂ S) (hf : S' ≃ S)
+  : Set.Infinite S := by
+  sorry
+
+/-- #### Corollary 6D (b)
+
+The set `ω` is infinite.
+-/
+theorem corollary_6d_b
+  : Set.Infinite (@Set.univ ℕ) := by
+  sorry
+
+/-- #### Corollary 6E
+
+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
+  sorry
+
+/-- #### Lemma 6F
+
+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)
+  : ∃ m : ℕ, m < n ∧ ∃ f : C → Fin m, Function.Bijective f := by
+  sorry
+
 /-- #### Exercise 6.1
 
 Show that the equation