From 21a3e78106fb6e989e88066359585f2573c49794 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 11 Aug 2023 15:23:32 -0600 Subject: [PATCH] Enderton (set). Continue refining ordering theorems/exercises. --- Bookshelf/Enderton/Set.tex | 250 +++++++++++++++++++++++--- Bookshelf/Enderton/Set/Chapter_4.lean | 191 +++++++++++++++++++- Common/Set/Basic.lean | 18 ++ 3 files changed, 428 insertions(+), 31 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 0988e93..26fd491 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -6863,6 +6863,8 @@ \code{Bookshelf/Enderton/Set/Chapter\_4} {Enderton.Set.Chapter\_4.zero\_least\_nat} + \lean{Std/Data/Nat/Init/Lemmas}{Nat.pos\_of\_ne\_zero} + \begin{proof} Let $$S = \{n \in \omega \mid n = 0 \lor 0 \in n\}.$$ @@ -7255,7 +7257,7 @@ \end{proof} -\subsection{\pending{% +\subsection{\verified{% Well Ordering of \texorpdfstring{$\omega$}{Natural Numbers}}}% \hyperlabel{sub:well-ordering-natural-numbers} @@ -7264,6 +7266,9 @@ Then there is some $m \in A$ such that $m \ineq n$ for all $n \in A$. \end{theorem} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.well\_ordering\_nat} + \lean{Mathlib/SetTheory/Ordinal/Basic}{WellOrder} \begin{note} @@ -7295,16 +7300,13 @@ \hyperlabel{par:well-ordering-natural-numbers-ii} Suppose $n \in S$. - That is, for all $m \in n$, $m \in \omega - A$. - Let $p$ be an arbitrary element of $A$. - By the \nameref{sub:trichotomy-law-natural-numbers}, only one of the - following holds: - $$p \in n^+, \quad p = n^+, \quad n^+ \in p.$$ - It cannot be that $p \in n^+$ since $p \in \omega - A$ by - \eqref{sub:well-ordering-natural-numbers-eq1}. - But then $n^+ = p$ or $n^+ \in p$, implying that $n^+$ is a least element - of $A$. - Since $A$ does not have a least element, it must be that $n^+ \not\in A$. + We want to prove that $$\forall m, m \in n^+ \Rightarrow m \not\in A.$$ + To this end, let $m \in \omega$ such that $m \in n^+$. + By definition of the \nameref{ref:successor}, $m \in n$ or $m = n$. + If the former, $n \in S$ implies $m \not\in A$. + If the latter, it isn't possible for $n \in A$ since the + \nameref{sub:trichotomy-law-natural-numbers} would otherwise imply + $n$ is the least element of $A$, which is assumed to not exist. Hence $n^+ \in S$. \paragraph{Conclusion}% @@ -7333,7 +7335,7 @@ Therefore it isn't possible $f(n^+) \in f(n)$ for all $n \in \omega$. \end{proof} -\subsection{\pending{% +\subsection{\verified{% Strong Induction Principle for \texorpdfstring{$\omega$}{Natural Numbers}}}% \hyperlabel{sub:strong-induction-principle-natural-numbers} @@ -7347,6 +7349,9 @@ Then $A = \omega$. \end{theorem} + \code{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.strong\_induction\_principle\_nat} + \begin{proof} For the sake of contradiction, suppose $\omega - A$ is a nonempty set. By \nameref{sub:well-ordering-natural-numbers}, there exists a least element @@ -7861,12 +7866,15 @@ Refer to \nameref{sub:theorem-4k-5}. \end{proof} -\subsection{\pending{Exercise 4.17}}% +\subsection{\verified{Exercise 4.17}}% \hyperlabel{sub:exercise-4.17} Prove that $m^{n+p} = m^n \cdot m^p$. - \lean*{Data/Nat/Lemmas}{Nat.pow\_add} + \code*{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.exercise\_4\_17} + + \lean{Data/Nat/Lemmas}{Nat.pow\_add} \begin{proof} @@ -7929,15 +7937,97 @@ Therefore $$\img{\in_\omega^{-1}}{\{7, 8\}} = \{6, 7\}.$$ \end{proof} -\subsection{\sorry{Exercise 4.19}}% +\subsection{\verified{Exercise 4.19}}% \hyperlabel{sub:exercise-4.19} Prove that if $m$ is a natural number and $d$ is a nonzero number, then there - exist numbers $q$ and $r$ such that $m = (d \cdot q) + r$ and $r$ is less than - $d$. + exist numbers $q$ and $r$ such that $m = (d \cdot q) + r$ and $r$ is less + than $d$. + + \code*{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.exercise\_4\_19} \begin{proof} - TODO + + Let $d \in \omega$ such that $d \neq 0$. + Define + \begin{equation} + \hyperlabel{sub:exercise-4.18-eq1} + S = \{m \in \omega \mid + (\exists q, d \in \omega) m = (d \cdot q) + r \land r < d\}. + \end{equation} + We prove that $S$ is an \nameref{ref:inductive-set} by showing + (i) $0 \in S$ and (ii) if $m \in S$, then $m^+ \in S$. + Afterward we prove (iii) the theorem statement. + + \paragraph{(i)}% + \hyperlabel{par:exercise-4.19-i} + + Let $q = 0$ and $r = 0$. + We note $r < d$ by \textref{sub:zero-least-natural-number}. + Furthermore, + \begin{align*} + (d \cdot 0) + 0 + & = d \cdot 0 & \textref{sub:theorem-4i} \\ + & = 0. & \textref{sub:theorem-4j} + \end{align*} + Thus $0 \in S$. + + \paragraph{(ii)}% + \hyperlabel{par:exercise-4.19-ii} + + Suppose $m \in S$. + Then there exists $q, d \in \omega$ such that $m = (d \cdot q) + r$ and + $r < d$. + Then + \begin{align*} + m^+ + & = ((d \cdot q) + r)^+ \\ + & = (d \cdot q) + r^+. & \textref{sub:theorem-4i} + \end{align*} + By \nameref{sub:trichotomy-law-natural-numbers}, there are three cases to + consider: + + \subparagraph{Case 1}% + + Suppose $r^+ \in d$. + Then it immediately follows $m^+ \in S$. + + \subparagraph{Case 2}% + + Suppose $r^+ = d$. + Then + \begin{align*} + m^+ + & = (d \cdot q) + r^+ \\ + & = (d \cdot q) + d \\ + & = d \cdot q^+ & \textref{sub:theorem-4j} \\ + & = (d \cdot q^+) + 0. & \textref{sub:theorem-4i} + \end{align*} + Hence $m^+ \in S$. + + \subparagraph{Case 3}% + + Suppose $d \in r^+$. + Then, by definition of the \nameref{ref:successor}, $d \in r$ or + $d = r$. + But $r \in d$. + Thus, by \nameref{sub:trichotomy-law-natural-numbers}, a contradiction + is introduced. + Hence this case is not possible. + + \subparagraph{Conclusion}% + + Since the above cases are exhaustive, it follows $m^+ \in S$. + + \paragraph{(iii)}% + + By \nameref{par:exercise-4.19-i} and \nameref{par:exercise-4.19-ii}, + $S \subseteq \omega$ is indeed an inductive set. + By \nameref{sub:theorem-4b}, $S = \omega$. + Thus for all $m, d \in \omega$ where $d \neq 0$, there exist numbers $q$ + and $r$ such that $m = (d \cdot q) + r$ and $r < d$. + \end{proof} \subsection{\sorry{Exercise 4.20}}% @@ -7950,44 +8040,148 @@ TODO \end{proof} -\subsection{\sorry{Exercise 4.21}}% +\subsection{\unverified{Exercise 4.21}}% \hyperlabel{sub:exercise-4.21} Show that no natural number is a subset of any of its elements. \begin{proof} - TODO + Let $n$ be a natural number. + Suppose $m \in n$. + By \nameref{sub:trichotomy-law-natural-numbers}, $n \neq m$ and + $n \not\in m$. + By \nameref{sub:corollary-4m}, $n \not\subseteq m$. \end{proof} -\subsection{\sorry{Exercise 4.22}}% +\subsection{\verified{Exercise 4.22}}% \hyperlabel{sub:exercise-4.22} Show that for any natural numbers $m$ and $p$ we have $m \in m + p^+$. + \code*{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.exercise\_4\_22} + \begin{proof} - TODO + + Let $m$ be a natural number and $$S = \{p \in \omega \mid m \in m + p^+\}.$$ + We prove that (i) $0 \in S$ and (ii) if $p \in S$, then $p^+ \in S$. + Afterward we prove (iii) the theorem statement. + + \paragraph{(i)}% + \hyperlabel{par:exercise-4.22-i} + + By definition of the \nameref{ref:successor}, $m^+ = m \cup \{m\}$. + Thus $m \in m^+ = m + 1$ (by \nameref{sub:successor-identity}). + Hence $0 \in S$. + + \paragraph{(ii)}% + \hyperlabel{par:exercise-4.22-ii} + + Suppose $p \in S$. + That is, $m \in m + p^+$. + By definition of the \nameref{ref:successor}, + \begin{align*} + m + p^+ + & \in (m + p^+) \cup \{m + p^+\} \\ + & = (m + p^+)^+ \\ + & = m + p^{++}. & \textref{sub:theorem-4i}. + \end{align*} + By \nameref{sub:theorem-4f}, $m + p^{++}$ is a + \nameref{ref:transitive-set}. + Therefore $m \in m + p^+ \in m + p^{++}$ implies $m \in m + p^{++}$. + Hence $p^+ \in S$. + + \paragraph{(iii)}% + + By \nameref{par:exercise-4.22-i} and \nameref{par:exercise-4.22-ii}, + $S \subseteq \omega$ is an inductive set. + Thus \nameref{sub:theorem-4b} implies $S = \omega$. + Hence for any natural numbers $m$ and $p$, we have $m \in m + p^+$. + \end{proof} -\subsection{\sorry{Exercise 4.23}}% +\subsection{\verified{Exercise 4.23}}% \hyperlabel{sub:exercise-4.23} Assume that $m$ and $n$ are natural numbers with $m$ less than $n$. Show that there is some $p$ in $\omega$ for which $m + p^+ = n$. - (It follows form this and the preceding exercise that $m$ is less than $n$ iff + (It follows from this and the preceding exercise that $m$ is less than $n$ iff $(\exists p \in \omega)m + p^+ = n$.) + \code*{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.exercise\_4\_23} + \begin{proof} - TODO + + Let $$S = \{n \in \omega \mid + (\forall m \in n, \exists p \in \omega) m + p^+ = n\}.$$ + We prove that (i) $0 \in S$ and (ii) if $p \in S$, then $p^+ \in S$. + Afterward we prove (iii) the theorem statement. + + \paragraph{(i)}% + \hyperlabel{par:exercise-4.23-i} + + It vacuously holds that $0 \in S$. + + \paragraph{(ii)}% + \hyperlabel{par:exercise-4.23-ii} + + Suppose $n \in S$. + Let $m \in n^+$. + By definition of the \nameref{ref:successor}, $m \in n$ or $m = n$. + If $m \in n$, then there exists some $p \in \omega$ such that + $m + p^+ = n$. + But then \nameref{sub:theorem-4i} implies + \begin{align*} + n^+ + & = (m + p^+)^+ \\ + & = m + p^{++}. + \end{align*} + If instead $m = n$, then \nameref{sub:successor-identity} implies that + $$n^+ = m^+ = m + 1 = m + 0^+.$$ + Hence $n^+ \in S$. + + \paragraph{(iii)}% + + By \nameref{par:exercise-4.23-i} and \nameref{par:exercise-4.23-ii}, $S$ + is an \nameref{ref:inductive-set}. + By \nameref{sub:theorem-4b}, $S = \omega$. + Thus for all $m, n \in \omega$ such that $m \in n$, there exists some + $p \in \omega$ such that $m + p^+ = n$. + \end{proof} -\subsection{\sorry{Exercise 4.24}}% +\subsection{\verified{Exercise 4.24}}% \hyperlabel{sub:exercise-4.24} Assume that $m + n = p + q$. - Show that $$m \in p \iff n \in q.$$ + Show that $$m \in p \iff q \in n.$$ + + \code*{Bookshelf/Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.exercise\_4\_24} \begin{proof} - TODO + + Let $m, n, p, q \in \omega$ such that $m + n = p + q$. + + \paragraph{($\Rightarrow$)}% + + Suppose $m \in p$. + By \nameref{sub:theorem-4n}, $m + n \in p + n$. + By hypothesis, $m + n = p + q$ meaning $p + q \in p + n$. + By \nameref{sub:theorem-4k-2}, $q + p \in n + p$. + Therefore another application of \nameref{sub:theorem-4n} implies + $q \in n$. + + \paragraph{($\Leftarrow$)}% + + Suppose $q \in n$. + By \nameref{sub:theorem-4n}, $q + p \in n + p$. + By \nameref{sub:theorem-4k-2}, $p + q \in p + n$. + By hypothesis, $p + q = m + n$ meaning $m + n \in p + n$. + Therefore another application of \nameref{sub:theorem-4n} implies + $m \in p$. + \end{proof} \subsection{\sorry{Exercise 4.25}}% diff --git a/Bookshelf/Enderton/Set/Chapter_4.lean b/Bookshelf/Enderton/Set/Chapter_4.lean index ccf43f5..7a2060a 100644 --- a/Bookshelf/Enderton/Set/Chapter_4.lean +++ b/Bookshelf/Enderton/Set/Chapter_4.lean @@ -1,5 +1,7 @@ import Common.Logic.Basic +import Common.Set.Basic import Mathlib.Data.Set.Basic +import Mathlib.SetTheory.Ordinal.Basic /-! # Enderton.Set.Chapter_4 @@ -280,6 +282,8 @@ theorem zero_least_nat (n : ℕ) rw [hm] exact Nat.succ_pos m +#check Nat.pos_of_ne_zero + /-! #### Theorem 4N For any natural numbers `n`, `m`, and `p`, @@ -386,7 +390,52 @@ Let `A` be a nonempty subset of `ω`. Then there is some `m ∈ A` such that -/ theorem well_ordering_nat (A : Set ℕ) (hA : Set.Nonempty A) : ∃ m ∈ A, ∀ n, n ∈ A → m ≤ n := by - sorry + -- Assume `A` does not have a least element. + by_contra nh + simp only [not_exists, not_and, not_forall, not_le, exists_prop] at nh + + -- If we show the complement of `A` is `ω`, then `A = ∅`, a contradiction. + suffices A.compl = Set.univ by + have h := Set.univ_diff_compl_eq_self A + rw [this] at h + simp only [sdiff_self, Set.bot_eq_empty] at h + exact absurd h.symm (Set.Nonempty.ne_empty hA) + + -- Use strong induction to prove every element of `ω` is in the complement. + have : ∀ n : ℕ, (∀ m, m < n → m ∈ A.compl) := by + intro n + induction n with + | zero => + intro m hm + exact False.elim (Nat.not_lt_zero m hm) + | succ n ih => + intro m hm + have hm' : m < n ∨ m = n := by + rw [Nat.lt_succ] at hm + exact Nat.lt_or_eq_of_le hm + apply Or.elim hm' + · intro h + exact ih m h + · intro h + have : ∀ x : ℕ, x ∈ A → n ≤ x := by + intro x hx + exact match @trichotomous ℕ LT.lt _ n x with + | Or.inl h₁ => Nat.le_of_lt h₁ + | Or.inr (Or.inl h₁) => Nat.le_of_eq h₁ + | Or.inr (Or.inr h₁) => False.elim (ih x h₁ hx) + by_cases hn : n ∈ A + · have ⟨p, hp⟩ := nh n hn + exact absurd hp.left (ih p hp.right) + · rw [h] + exact hn + + ext x + simp only [Set.mem_univ, iff_true] + by_contra nh' + have ⟨y, hy₁, hy₂⟩ := nh x (show x ∈ A from Set.not_not_mem.mp nh') + exact absurd hy₁ (this x y hy₂) + +#check WellOrder /-- #### Strong Induction Principle for ω @@ -394,9 +443,23 @@ Let `A` be a subset of `ω`, and assume that for every `n ∈ ω`, if every numb less than `n` is in `A`, then `n ∈ A`. Then `A = ω`. -/ theorem strong_induction_principle_nat (A : Set ℕ) - (h : ∀ n : ℕ, (∀ m : ℕ, m < n → m ∈ A) → n ∈ A) + (h : ∀ n : ℕ, (∀ x : ℕ, x < n → x ∈ A) → n ∈ A) : A = Set.univ := by - sorry + suffices A.compl = ∅ by + have h' := Set.univ_diff_compl_eq_self A + rw [this] at h' + simp only [Set.diff_empty] at h' + exact h'.symm + + by_contra nh + have ⟨m, hm⟩ := well_ordering_nat A.compl (Set.nmem_singleton_empty.mp nh) + refine absurd (h m ?_) hm.left + + -- Show that every number less than `m` is in `A`. + intro x hx + by_contra nx + have : x < x := Nat.lt_of_lt_of_le hx (hm.right x nx) + simp at this /-- #### Exercise 4.1 @@ -485,4 +548,126 @@ theorem exercise_4_14 (n : ℕ) have : even n := ⟨q, hq'⟩ exact absurd this h +/-- #### Exercise 4.17 + +Prove that `mⁿ⁺ᵖ = mⁿ ⬝ mᵖ.` +-/ +theorem exercise_4_17 (m n p : ℕ) + : m ^ (n + p) = m ^ n * m ^ p := by + induction p with + | zero => calc m ^ (n + 0) + _ = m ^ n := rfl + _ = m ^ n * 1 := by rw [right_mul_id] + _ = m ^ n * m ^ 0 := rfl + | succ p ih => calc m ^ (n + p.succ) + _ = m ^ (n + p).succ := rfl + _ = m ^ (n + p) * m := rfl + _ = m ^ n * m ^ p * m := by rw [ih] + _ = m ^ n * (m ^ p * m) := by rw [theorem_4k_4] + _ = m ^ n * m ^ p.succ := rfl + +/-- #### Exercise 4.19 + +Prove that if `m` is a natural number and `d` is a nonzero number, then there +exist numbers `q` and `r` such that `m = (d ⬝ q) + r` and `r` is less than `d`. +-/ +theorem exercise_4_19 (m d : ℕ) (hd : d ≠ 0) + : ∃ q r : ℕ, m = (d * q) + r ∧ r < d := by + induction m with + | zero => + refine ⟨0, 0, ?_⟩ + simp only [Nat.zero_eq, mul_zero, add_zero, true_and] + exact Nat.pos_of_ne_zero hd + | succ m ih => + have ⟨q, r, hm, hr⟩ := ih + have hm' := calc m.succ + _ = ((d * q) + r).succ := by rw [hm] + _ = (d * q) + r.succ := rfl + match @trichotomous ℕ LT.lt _ r.succ d with + | Or.inl h₁ => + exact ⟨q, r.succ, hm', h₁⟩ + | Or.inr (Or.inl h₁) => + refine ⟨q.succ, 0, ?_, Nat.pos_of_ne_zero hd⟩ + calc Nat.succ m + _ = d * q + Nat.succ r := hm' + _ = d * q + d := by rw [h₁] + _ = d * q.succ := rfl + _ = d * q.succ + 0 := rfl + | Or.inr (Or.inr h₁) => + have : d < d := calc d + _ ≤ r := Nat.lt_succ.mp h₁ + _ < d := hr + simp at this + +/-- #### Exercise 4.22 + +Show that for any natural numbers `m` and `p` we have `m ∈ m + p⁺`. +-/ +theorem exercise_4_22 (m p : ℕ) + : m < m + p.succ := by + induction p with + | zero => simp + | succ p ih => calc m + _ < m + p.succ := ih + _ < m + p.succ.succ := Nat.lt.base (m + p.succ) + +/-- #### Exercise 4.23 + +Assume that `m` and `n` are natural numbers with `m` less than `n`. Show that +there is some `p` in `ω` for which `m + p⁺ = n`. (It follows from this and the +preceding exercise that `m` is less than `n` iff (`∃p ∈ ω) m + p⁺ = n`.) +-/ +theorem exercise_4_23 (m n : ℕ) (hm : m < n) + : ∃ p : ℕ, m + p.succ = n := by + induction n with + | zero => simp at hm + | succ n ih => + have : m < n ∨ m = n := by + rw [Nat.lt_succ] at hm + exact Nat.lt_or_eq_of_le hm + apply Or.elim this + · intro hm₁ + have ⟨p, hp⟩ := ih hm₁ + refine ⟨p.succ, ?_⟩ + exact Eq.symm $ calc n.succ + _ = (m + p.succ).succ := by rw [← hp] + _ = m + p.succ.succ := rfl + · intro hm₁ + refine ⟨0, ?_⟩ + rw [hm₁] + +/-- #### Exercise 4.24 + +Assume that `m + n = p + q`. Show that +``` +m ∈ p ↔ q ∈ n. +``` +-/ +theorem exercise_4_24 (m n p q : ℕ) (h : m + n = p + q) + : m < p ↔ q < n := by + apply Iff.intro + · intro hm + have hr : m + n < p + n := (theorem_4n_i m p n).mp hm + rw [h] at hr + conv at hr => left; rw [add_comm] + conv at hr => right; rw [add_comm] + exact (theorem_4n_i q n p).mpr hr + · intro hq + have hr : q + p < n + p := (theorem_4n_i q n p).mp hq + conv at hr => left; rw [add_comm] + conv at hr => right; rw [add_comm] + rw [← h] at hr + exact (theorem_4n_i m p n).mpr hr + +/-- #### Exercise 4.25 + +Assume that `n ∈ m` and `q ∈ p`. Show that +``` +(m ⬝ q) + (n ⬝ p) ∈ (m ⬝ p) + (n ⬝ q). +``` +-/ +theorem exercise_4_25 (m n p q : ℕ) (h₁ : n < m) (h₂ : q < p) + : (m * q) + (n * p) < (m * p) + (n * q) := by + sorry + end Enderton.Set.Chapter_4 \ No newline at end of file diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index aec46e6..dcb5eff 100644 --- a/Common/Set/Basic.lean +++ b/Common/Set/Basic.lean @@ -154,6 +154,24 @@ theorem prod_nonempty_nonempty_imp_nonempty_prod {A : Set α} {B : Set β} rw [← nonempty_iff_ne_empty, ← nonempty_iff_ne_empty] exact ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ +/-! ## Difference -/ + +/-- +For any set `A`, the difference between the sample space and `A` is the +complement of `A`. +-/ +theorem univ_diff_self_eq_compl (A : Set α) : Set.univ \ A = A.compl := by + unfold Set.compl SDiff.sdiff instSDiffSet Set.diff + simp only [mem_univ, true_and] + +/-- +For any set `A`, the difference between the sample space and the complement of +`A` is `A`. +-/ +theorem univ_diff_compl_eq_self (A : Set α) : Set.univ \ A.compl = A := by + unfold Set.compl SDiff.sdiff instSDiffSet Set.diff + simp only [mem_univ, mem_setOf_eq, not_not, true_and, setOf_mem_eq] + /-! ## Symmetric Difference -/ /--