From 656530fed9dbe797c306af2c3c6a1493a7504f6b Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 11 Aug 2023 08:17:30 -0600 Subject: [PATCH] Enderton (set). Theorem 4N, Corollary 4P. --- Bookshelf/Enderton/Set.tex | 43 +++++---- Bookshelf/Enderton/Set/Chapter_4.lean | 121 +++++++++++++++++++++++--- 2 files changed, 136 insertions(+), 28 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index da6338c..0988e93 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -6895,7 +6895,7 @@ \end{proof} -\subsection{\verified{% +\subsection{\unverified{% Trichotomy Law for \texorpdfstring{$\omega$}{Natural Numbers}}}% \hyperlabel{sub:trichotomy-law-natural-numbers} @@ -6904,8 +6904,9 @@ $$m \in n, \quad m = n, \quad n \in m$$ holds. \end{theorem} - \code{Bookshelf/Enderton/Set/Chapter\_4} - {Enderton.Set.Chapter\_4.trichotomy\_law\_for\_nat} + \lean{Mathlib/Order/RelClasses}{IsAsymm} + + \lean{Mathlib/Init/Algebra/Classes}{IsTrichotomous} \begin{proof} @@ -6974,7 +6975,7 @@ \end{proof} -\subsection{\verified{% +\subsection{\unverified{% Linear Ordering on \texorpdfstring{$\omega$}{Natural Numbers}}}% \hyperlabel{sub:linear-ordering-natural-numbers} @@ -6987,8 +6988,8 @@ is a linear ordering on $\omega$. \end{theorem} - \code{Bookshelf/Enderton/Set/Chapter\_4} - {Enderton.Set.Chapter\_4.linear\_ordering\_on\_nat} + \lean{Mathlib/Init/Algebra/Order} + {LinearOrder.isStrictTotalOrder\_of\_linearOrder} \begin{proof} @@ -7083,23 +7084,32 @@ \end{proof} -\subsection{\pending{Theorem 4N}}% +\subsection{\verified{Theorem 4N}}% \hyperlabel{sub:theorem-4n} \begin{theorem}[4N] - For any natural numbers $n$, $m$, and $p$, $$m \in n \iff m + p \in n + p.$$ - If, in addition, $p \neq 0$, then $$m \in n \iff m \cdot p \in n \cdot p.$$ + For any natural numbers $n$, $m$, and $p$, + \begin{equation} + m \in n \iff m + p \in n + p. \tag{i} + \end{equation} + If, in addition, $p \neq 0$, then + \begin{equation} + m \in n \iff m \cdot p \in n \cdot p. \tag{ii} + \end{equation} \end{theorem} + \code{Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4n\_i} + \lean{Std/Data/Nat/Lemmas}{Nat.add\_lt\_add\_iff\_right} + \code{Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.theorem\_4n\_ii} + \lean{Init/Data/Nat/Basic}{Nat.mul\_lt\_mul\_of\_pos\_right} \begin{proof} - We prove that (i) $m \in n$ iff $m + p \in n + p$ and, - (ii) if $p \neq 0$, then $m \in n$ iff $m \cdot p \in n \cdot p$. - \paragraph{(i)}% \hyperlabel{par:theorem-4n-i} @@ -7197,7 +7207,7 @@ \end{proof} -\subsection{\pending{Corollary 4P}}% +\subsection{\verified{Corollary 4P}}% \hyperlabel{sub:corollary-4p} \begin{corollary}[4P] @@ -7210,10 +7220,13 @@ \end{align} \end{corollary} - \code{Common/Nat/Basic}{Nat.mul\_right\_cancel} + \code{Enderton/Set/Chapter\_4} + {Enderton.Set.Chapter\_4.corollary\_4p\_i} \lean{Init/Data/Nat/Basic}{Nat.add\_right\_cancel} + \code{Common/Nat/Basic}{Nat.mul\_right\_cancel} + \begin{proof} \paragraph{\eqref{sub:corollary-4p-eq1}}% @@ -7320,7 +7333,7 @@ Therefore it isn't possible $f(n^+) \in f(n)$ for all $n \in \omega$. \end{proof} -\subsection{\sorry{% +\subsection{\pending{% Strong Induction Principle for \texorpdfstring{$\omega$}{Natural Numbers}}}% \hyperlabel{sub:strong-induction-principle-natural-numbers} diff --git a/Bookshelf/Enderton/Set/Chapter_4.lean b/Bookshelf/Enderton/Set/Chapter_4.lean index 8659b7d..ccf43f5 100644 --- a/Bookshelf/Enderton/Set/Chapter_4.lean +++ b/Bookshelf/Enderton/Set/Chapter_4.lean @@ -280,28 +280,123 @@ theorem zero_least_nat (n : ℕ) rw [hm] exact Nat.succ_pos m -/-- #### Trichotomy Law for ω +/-! #### Theorem 4N -For any natural numbers `m` and `n`, exactly one of the three conditions +For any natural numbers `n`, `m`, and `p`, ``` -m ∈ n, m = n, n ∈ m +m ∈ n ↔ m ⬝ p ∈ n ⬝ p. +``` +If, in addition, `p ≠ 0`, then +``` +m ∈ n ↔ m ⬝ p ∈ n ⬝ p. ``` -holds. -/ -theorem trichotomy_law_for_nat - : IsAsymm ℕ LT.lt ∧ IsTrichotomous ℕ LT.lt := - ⟨instIsAsymmLtToLT, instIsTrichotomousLtToLTToPreorderToPartialOrder⟩ -/-- #### Linear Ordering on ω +theorem theorem_4n_i (m n p : ℕ) + : m < n ↔ m + p < n + p := by + have hf : ∀ m n : ℕ, m < n → m + p < n + p := by + induction p with + | zero => simp + | succ p ih => + intro m n hp + have := ih m n hp + rw [← Nat.succ_lt_succ_iff] at this + have h₁ : (m + p).succ = m + p.succ := rfl + have h₂ : (n + p).succ = n + p.succ := rfl + rwa [← h₁, ← h₂] + apply Iff.intro + · exact hf m n + · intro h + match @trichotomous ℕ LT.lt _ m n with + | Or.inl h₁ => + exact h₁ + | Or.inr (Or.inl h₁) => + rw [← h₁] at h + exact absurd h (lemma_4l_b (m + p)) + | Or.inr (Or.inr h₁) => + have := hf n m h₁ + exact absurd this (Nat.lt_asymm h) -Relation +#check Nat.add_lt_add_iff_right + +theorem theorem_4n_ii (m n p : ℕ) + : m < n ↔ m * p.succ < n * p.succ := by + have hf : ∀ m n : ℕ, m < n → m * p.succ < n * p.succ := by + intro m n hp₁ + induction p with + | zero => + simp only [Nat.mul_one] + exact hp₁ + | succ p ih => + have hp₂ : m * p.succ < n * p.succ := by + by_cases hp₃ : p = 0 + · rw [hp₃] at * + simp only [Nat.mul_one] at * + exact hp₁ + · exact ih + calc m * p.succ.succ + _ = m * p.succ + m := rfl + _ < n * p.succ + m := (theorem_4n_i (m * p.succ) (n * p.succ) m).mp hp₂ + _ = m + n * p.succ := by rw [theorem_4k_2] + _ < n + n * p.succ := (theorem_4n_i m n (n * p.succ)).mp hp₁ + _ = n * p.succ + n := by rw [theorem_4k_2] + _ = n * p.succ.succ := rfl + apply Iff.intro + · exact hf m n + · intro hp + match @trichotomous ℕ LT.lt _ m n with + | Or.inl h₁ => + exact h₁ + | Or.inr (Or.inl h₁) => + rw [← h₁] at hp + exact absurd hp (lemma_4l_b (m * p.succ)) + | Or.inr (Or.inr h₁) => + have := hf n m h₁ + exact absurd this (Nat.lt_asymm hp) + +#check Nat.mul_lt_mul_of_pos_right + +/-! #### Corollary 4P + +The following cancellation laws hold for `m`, `n`, and `p` in `ω`: ``` -∈_ω = {⟨m, n⟩ ∈ ω × ω | m ∈ n} +m + p = n + p ⇒ m = n, +m ⬝ p = n ⬝ p ∧ p ≠ 0 ⇒ m = n. ``` -is a linear ordering on `ω`. -/ -theorem linear_ordering_on_nat - : IsStrictTotalOrder ℕ LT.lt := isStrictTotalOrder_of_linearOrder + +theorem corollary_4p_i (m n p : ℕ) (h : m + p = n + p) + : m = n := by + match @trichotomous ℕ LT.lt _ m n with + | Or.inl h₁ => + rw [theorem_4n_i m n p, h] at h₁ + exact absurd h₁ (lemma_4l_b (n + p)) + | Or.inr (Or.inl h₁) => + exact h₁ + | Or.inr (Or.inr h₁) => + rw [theorem_4n_i n m p, h] at h₁ + exact absurd h₁ (lemma_4l_b (n + p)) + +#check Nat.add_right_cancel + +/-- #### Well Ordering of ω + +Let `A` be a nonempty subset of `ω`. Then there is some `m ∈ A` such that +`m ≤ n` for all `n ∈ A`. +-/ +theorem well_ordering_nat (A : Set ℕ) (hA : Set.Nonempty A) + : ∃ m ∈ A, ∀ n, n ∈ A → m ≤ n := by + sorry + +/-- #### Strong Induction Principle for ω + +Let `A` be a subset of `ω`, and assume that for every `n ∈ ω`, if every number +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) + : A = Set.univ := by + sorry /-- #### Exercise 4.1