From f40e1fddaaaa6e9d19d09b28028afa475c9d4fec Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 8 Aug 2023 08:56:13 -0600 Subject: [PATCH] Enderton. Corollary 4P. --- Bookshelf/Enderton/Set.tex | 70 +++++++++++++++++++++++++------------- Common.lean | 1 + Common/Nat.lean | 1 + Common/Nat/Basic.lean | 24 +++++++++++++ 4 files changed, 72 insertions(+), 24 deletions(-) create mode 100644 Common/Nat.lean create mode 100644 Common/Nat/Basic.lean diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 86c6204..912efc8 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -7623,26 +7623,22 @@ Show that $<_L$ is a linear ordering on $A \times B$. \subparagraph{($\Leftarrow$)}% Let $p$ be a natural number and suppose $m + p \in n + p$. - By the \nameref{sub:trichotomy-law-natural-numbers}, there are three - ways $m$ and $n$ may relate to one another. + By the \nameref{sub:trichotomy-law-natural-numbers}, there are two + cases to consider regarding how $m$ and $n$ relate to one another: \vspace{8pt} - \textbf{Case 1}: Suppose $m \in n$. - Then our proof is complete. - - \vspace{8pt} - \textbf{Case 2}: Suppose $m = n$. + \textbf{Case 1}: Suppose $m = n$. Then $m + p \in n + p = m + p$. \nameref{sub:lemma-4l-b} shows this is impossible. \vspace{8pt} - \textbf{Case 3}: Suppose $n \in m$. + \textbf{Case 2}: Suppose $n \in m$. Then \nameref{spar:theorem-4n-i-right} indicates $n + p \in m + p$. But this contradicts \nameref{sub:trichotomy-law-natural-numbers} since, by hypothesis, $m + p \in n + p$. \vspace{8pt} - \textbf{Conclusion}: The only possibility is $m \in n$. + \textbf{Conclusion}: By trichotomy, it follows $m \in n$. \paragraph{(ii)}% \hyperlabel{par:theorem-4n-ii} @@ -7679,46 +7675,72 @@ Show that $<_L$ is a linear ordering on $A \times B$. \subparagraph{($\Leftarrow$)}% Let $p \neq 0$ be a natural number and suppose $m \cdot p \in n \cdot p$. - By the \nameref{sub:trichotomy-law-natural-numbers}, there are three - ways $m$ and $n$ may relate to one another. + By the \nameref{sub:trichotomy-law-natural-numbers}, there are two + cases to consider regarding how $m$ and $n$ relate to one another: \vspace{8pt} - \textbf{Case 1}: Suppose $m \in n$. - Then our proof is complete. - - \vspace{8pt} - \textbf{Case 2}: Suppose $m = n$. + \textbf{Case 1}: Suppose $m = n$. Then $m \cdot p \in n \cdot p = m \cdot p$. \nameref{sub:lemma-4l-b} shows this is impossible. \vspace{8pt} - \textbf{Case 3}: Suppose $n \in m$. + \textbf{Case 2}: Suppose $n \in m$. Then \nameref{spar:theorem-4n-ii-right} indicates $n \cdot p \in m \cdot p$. But this contradicts \nameref{sub:trichotomy-law-natural-numbers} since, by hypothesis, $m \cdot p \in n \cdot p$. \vspace{8pt} - \textbf{Conclusion}: The only possibility is $m \in n$. + \textbf{Conclusion}: By trichotomy, it follows $m \in n$. \end{proof} -\subsection{\sorry{Corollary 4P}}% +\subsection{\verified{Corollary 4P}}% \hyperlabel{sub:corollary-4p} \begin{corollary}[4P] The following cancellation laws hold for $m$, $n$, and $p$ in $\omega$: - \begin{align*} - m + p = n + p & \Rightarrow m = n, \\ - m \cdot p = n \cdot p & \Rightarrow m = n. - \end{align*} + \begin{align} + m + p = n + p & \Rightarrow m = n, + & \hyperlabel{sub:corollary-4p-eq1} \\ + m \cdot p = n \cdot p \land p \neq 0 & \Rightarrow m = n. + & \hyperlabel{sub:corollary-4p-eq2} + \end{align} \end{corollary} \begin{proof} - TODO + \statementpadding + + \lean*{Init/Data/Nat/Basic}{Nat.add\_right\_cancel} + + \lean{Common/Nat/Basic}{Nat.mul\_right\_cancel} + + \paragraph{\eqref{sub:corollary-4p-eq1}}% + + Suppose $m + p = n + p$. + By the \nameref{sub:trichotomy-law-natural-numbers}, there are two + cases to consider regarding how $m$ and $n$ relate to one another. + If $m \in n$, then \nameref{sub:theorem-4n} implies $m + p \in n + p$. + If $n \in m$, then \nameref{sub:theorem-4n} implies $n + p \in m + p$. + Both of these contradict the \nameref{sub:trichotomy-law-natural-numbers} of + $m + p$ and $n + p$. + Thus $m = n$ is the only remaining possibility. + + \paragraph{\eqref{sub:corollary-4p-eq2}}% + + Suppose $m \cdot p = n \cdot p$ and $p \neq 0$. + By the \nameref{sub:trichotomy-law-natural-numbers}, there are two + cases to consider regarding how $m$ and $n$ relate to one another. + If $m \in n$, then \nameref{sub:theorem-4n} implies + $m \cdot p \in n \cdot p$. + If $n \in m$, then \nameref{sub:theorem-4n} implies + $n \cdot p \in m \cdot p$. + Both of these contradict the \nameref{sub:trichotomy-law-natural-numbers} of + $m \cdot p$ and $n \cdot p$. + Thus $m = n$ is the only remaining possibility. \end{proof} diff --git a/Common.lean b/Common.lean index bd5e5a0..7dc8887 100644 --- a/Common.lean +++ b/Common.lean @@ -1,4 +1,5 @@ import Common.List import Common.Logic +import Common.Nat import Common.Real import Common.Set \ No newline at end of file diff --git a/Common/Nat.lean b/Common/Nat.lean new file mode 100644 index 0000000..82e1170 --- /dev/null +++ b/Common/Nat.lean @@ -0,0 +1 @@ +import Common.Nat.Basic \ No newline at end of file diff --git a/Common/Nat/Basic.lean b/Common/Nat/Basic.lean new file mode 100644 index 0000000..9af48ad --- /dev/null +++ b/Common/Nat/Basic.lean @@ -0,0 +1,24 @@ +import Mathlib.Data.Set.Basic + +namespace Nat + +/-- +The following cancellation law holds for `m`, `n`, and `p` in `ω`: +``` +m ⬝ p = n ⬝ p ∧ p ≠ 0 → m = n +``` +-/ +theorem mul_right_cancel (m n p : ℕ) (hp : 0 < p) : m * p = n * p → m = n := by + intro hmn + match @trichotomous ℕ LT.lt _ m n with + | Or.inl h => + have : m * p < n * p := Nat.mul_lt_mul_of_pos_right h hp + rw [hmn] at this + simp at this + | Or.inr (Or.inl h) => exact h + | Or.inr (Or.inr h) => + have : n * p < m * p := Nat.mul_lt_mul_of_pos_right h hp + rw [hmn] at this + simp at this + +end Nat \ No newline at end of file