diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 7987458..58a72c6 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -9304,8 +9304,8 @@ \begin{lemma} Let $A \equin m$ for some natural number $m$ and $B \subseteq A$. - Then there exists some $n \in \omega$ such that $n \leq m$, $B \equin n$ and - $A - B \equin m - n$. + Then there exists some $n \in \omega$ such that $n \leq m$, $B \equin n$, + and $A - B \equin m - n$. \end{lemma} \code{Bookshelf/Enderton/Set/Chapter\_6} @@ -9384,7 +9384,7 @@ & = (A - B) - \{a\} & \eqref{par:set-difference-size-ii-eq2} \\ & = A - B \\ & \equin m - n & \eqref{par:set-difference-size-ii-eq1} \\ - & \equin m^+ - n^+ & \textref{sub:theorem-6a}. + & \equin m^+ - n^+. \end{align*} \subparagraph{Case 2}% @@ -9400,8 +9400,7 @@ between $(A - \{a\}) - B$ and $m - n$. Therefore $g \cup \{\tuple{a, m}\}$ is a one-to-one correspondence between $A - B$ and $(m - n) \cup \{m\}$. - By \nameref{sub:theorem-6a}, - $$A - B \equin (m - n) \cup \{m\} \equin m^+ - n.$$ + Hence $$A - B \equin (m - n) \cup \{m\} \equin m^+ - n.$$ \subparagraph{Subconclusion}% diff --git a/Bookshelf/Enderton/Set/Chapter_6.lean b/Bookshelf/Enderton/Set/Chapter_6.lean index 711a148..2054d2d 100644 --- a/Bookshelf/Enderton/Set/Chapter_6.lean +++ b/Bookshelf/Enderton/Set/Chapter_6.lean @@ -1119,41 +1119,11 @@ lemma sdiff_size_aux [DecidableEq α] [Nonempty α] > `(A - {a} - (B - {a})) = (A - B) - {a}` > ` = A - B` > ` ≈ m - n` *(6.4)* -> ` ≈ m⁺ - n⁺` *(Theorem 6A)* +> ` ≈ m⁺ - n⁺` -/ rw [hA₁, hA₂] at hn₃ - suffices (Set.Iio m) \ (Set.Iio n) ≈ (Set.Iio m.succ) \ (Set.Iio n.succ) - from Set.equinumerous_trans hn₃ this - -- `m - n ≈ m⁺ - n⁺` - refine ⟨fun x => x + 1, ?_, ?_, ?_⟩ - · intro x ⟨hx₁, hx₂⟩ - simp at hx₁ hx₂ ⊢ - exact ⟨Nat.le_add_of_sub_le hx₂, Nat.add_lt_of_lt_sub hx₁⟩ - · intro _ _ _ _ h - simp only [add_left_inj] at h - exact h - · unfold Set.SurjOn Set.image - rw [Set.subset_def] - intro x ⟨hx₁, hx₂⟩ - simp only [ - Set.Iio_diff_Iio, - gt_iff_lt, - not_lt, - ge_iff_le, - Set.mem_setOf_eq, - Set.mem_Iio - ] at hx₁ hx₂ ⊢ - have ⟨p, hp⟩ : ∃ p : ℕ, x = p.succ := by - refine Nat.exists_eq_succ_of_ne_zero ?_ - have := calc 0 - _ < n.succ := by simp - _ ≤ x := hx₂ - exact Nat.pos_iff_ne_zero.mp this - refine ⟨p, ⟨?_, ?_⟩, hp.symm⟩ - · rw [hp] at hx₂ - exact Nat.lt_succ.mp hx₂ - · rw [hp] at hx₁ - exact Nat.succ_lt_succ_iff.mp hx₁ + exact Set.equinumerous_trans hn₃ + (Set.equinumerous_symm Set.succ_diff_succ_equinumerous_diff) /- > ##### Case 2 > Assume `a ∉ B`. Then `B - {a} = B` (i.e. `B ≈ n`) and @@ -1223,49 +1193,11 @@ lemma sdiff_size_aux [DecidableEq α] [Nonempty α] · exact ⟨hy₁.left.left, hy₁.right⟩ · rwa [if_neg hy₁.left.right] /- -> By *Theorem 6A* +> Hence > > `A - B ≈ (m - n) ∪ {m} ≈ m⁺ - n`. -/ - suffices (Set.Iio m) \ (Set.Iio n) ∪ {m} ≈ (Set.Iio m.succ) \ (Set.Iio n) - from Set.equinumerous_trans hAB this - refine ⟨fun x => x, ?_, ?_, ?_⟩ - · intro x hx - simp at hx ⊢ - apply Or.elim hx - · intro hx₁ - rw [hx₁] - exact ⟨hn₁, by simp⟩ - · intro ⟨hx₁, hx₂⟩ - exact ⟨hx₁, calc x - _ < m := hx₂ - _ < m + 1 := by simp⟩ - · intro _ _ _ _ h - exact h - · unfold Set.SurjOn Set.image - rw [Set.subset_def] - simp only [ - Set.Iio_diff_Iio, - gt_iff_lt, - not_lt, - ge_iff_le, - Set.mem_Ico, - Set.union_singleton, - lt_self_iff_false, - and_false, - Set.mem_insert_iff, - exists_eq_right, - Set.mem_setOf_eq, - and_imp - ] - intro x hn hm - apply Or.elim (Nat.lt_or_eq_of_lt hm) - · intro hx - right - exact ⟨hn, hx⟩ - · intro hx - left - exact hx + exact Set.equinumerous_trans hAB (Set.diff_union_equinumerous_succ_diff hn₁) /- > ##### Subconclusion > The above two cases are exhaustive and both conclude the existence of some diff --git a/Common/Set/Equinumerous.lean b/Common/Set/Equinumerous.lean index a59ca6e..eafbd31 100644 --- a/Common/Set/Equinumerous.lean +++ b/Common/Set/Equinumerous.lean @@ -1,3 +1,5 @@ +import Common.Nat.Basic +import Common.Set.Basic import Mathlib.Data.Finset.Card import Mathlib.Data.Set.Finite @@ -128,4 +130,82 @@ theorem equinumerous_emptyset_emptyset [Bot β] · unfold SurjOn simp +/-- +For all natural numbers `m, n`, `m⁺ - n⁺ ≈ m - n`. +-/ +theorem succ_diff_succ_equinumerous_diff {m n : ℕ} + : Set.Iio m.succ \ Set.Iio n.succ ≈ Set.Iio m \ Set.Iio n := by + refine Set.equinumerous_symm ⟨fun x => x + 1, ?_, ?_, ?_⟩ + · intro x ⟨hx₁, hx₂⟩ + simp at hx₁ hx₂ ⊢ + exact ⟨Nat.le_add_of_sub_le hx₂, Nat.add_lt_of_lt_sub hx₁⟩ + · intro _ _ _ _ h + simp only [add_left_inj] at h + exact h + · unfold Set.SurjOn Set.image + rw [Set.subset_def] + intro x ⟨hx₁, hx₂⟩ + simp only [ + Set.Iio_diff_Iio, + gt_iff_lt, + not_lt, + ge_iff_le, + Set.mem_setOf_eq, + Set.mem_Iio + ] at hx₁ hx₂ ⊢ + have ⟨p, hp⟩ : ∃ p : ℕ, x = p.succ := by + refine Nat.exists_eq_succ_of_ne_zero ?_ + have := calc 0 + _ < n.succ := by simp + _ ≤ x := hx₂ + exact Nat.pos_iff_ne_zero.mp this + refine ⟨p, ⟨?_, ?_⟩, hp.symm⟩ + · rw [hp] at hx₂ + exact Nat.lt_succ.mp hx₂ + · rw [hp] at hx₁ + exact Nat.succ_lt_succ_iff.mp hx₁ + +/-- +For all natural numbers `m, n`, `m - n ∪ {m} ≈ m - n`. +-/ +theorem diff_union_equinumerous_succ_diff {m n : ℕ} (hn: n ≤ m) + : Set.Iio m \ Set.Iio n ∪ {m} ≈ Set.Iio (Nat.succ m) \ Set.Iio n := by + refine ⟨fun x => x, ?_, ?_, ?_⟩ + · intro x hx + simp at hx ⊢ + apply Or.elim hx + · intro hx₁ + rw [hx₁] + exact ⟨hn, by simp⟩ + · intro ⟨hx₁, hx₂⟩ + exact ⟨hx₁, calc x + _ < m := hx₂ + _ < m + 1 := by simp⟩ + · intro _ _ _ _ h + exact h + · unfold Set.SurjOn Set.image + rw [Set.subset_def] + simp only [ + Set.Iio_diff_Iio, + gt_iff_lt, + not_lt, + ge_iff_le, + Set.mem_Ico, + Set.union_singleton, + lt_self_iff_false, + and_false, + Set.mem_insert_iff, + exists_eq_right, + Set.mem_setOf_eq, + and_imp + ] + intro x hn hm + apply Or.elim (Nat.lt_or_eq_of_lt hm) + · intro hx + right + exact ⟨hn, hx⟩ + · intro hx + left + exact hx + end Set