Enderton. Finish ordering relation exercises/theorems.

Bookshelf/Apostol.tex

@@ -185,8 +185,10 @@ That is to say, for each $k = 1, 2, \ldots, n$, there is a real number $s_k$
   such that $$s(x) = s_k \quad\text{if}\quad x_{k-1} < x < x_k.$$
   Step functions are sometimes called \textbf{piecewise constant functions}.
 
-\note{At each of the endpoints $x_{k-1}$ and $x_k$ the function must
+\begin{note}
-  have some well-defined value, but this need not be the same as $s_k$.}
+  At each of the endpoints $x_{k-1}$ and $x_k$ the function must have some
+  well-defined value, but this need not be the same as $s_k$.
+\end{note}
 
 \begin{definition}
 
@@ -478,7 +480,9 @@ Let $h$ be a given positive number and let $S$ be a set of real numbers.
 Given nonempty subsets $A$ and $B$ of $\mathbb{R}$, let $C$ denote the set
   $$C = \{a + b : a \in A, b \in B\}.$$
 
-\note{This is known as the "Additive Property."}
+\begin{note}
+  This is known as the "Additive Property."
+\end{note}
 
 \subsection{\verified{Theorem I.33a}}%
 \hyperlabel{sub:theorem-i.33a}
@@ -1609,8 +1613,10 @@ If $a$ and $b$ are positive integers with no common factor, we have the formula
   $$\sum_{n=1}^{b-1} \floor{\frac{na}{b}} = \frac{(a - 1)(b - 1)}{2}.$$
 When $b = 1$, the sum on the left is understood to be $0$.
 
-\note{When $b = 1$, the proofs of (a) and (b) are trivial. We continue under the
+\begin{note}
-  assumption $b > 1$.}
+  When $b = 1$, the proofs of (a) and (b) are trivial. We continue under the
+  assumption $b > 1$.
+\end{note}
 
 \subsubsection{\pending{Exercise 1.11.7a}}%
 \hyperlabel{ssub:exercise-1.11.7a}
@@ -2394,8 +2400,10 @@ Which of the following properties would remain valid in this new theory?
 
 $\int_a^b s + \int_b^c s = \int_a^c s$.
 
-\note{This property mirrors
+\begin{note}
-  \nameref{sub:step-additivity-with-respect-interval-integration}.}
+  This property mirrors
+    \nameref{sub:step-additivity-with-respect-interval-integration}.
+\end{note}
 
 \begin{proof}
 
@@ -2430,7 +2438,9 @@ $\int_a^b s + \int_b^c s = \int_a^c s$.
 
 $\int_a^b (s + t) = \int_a^b s + \int_a^b t$.
 
-\note{This property mirrors the \nameref{sub:step-additive-property}.}
+\begin{note}
+  This property mirrors the \nameref{sub:step-additive-property}.
+\end{note}
 
 \begin{proof}
 
@@ -2477,7 +2487,9 @@ $\int_a^b (s + t) = \int_a^b s + \int_a^b t$.
 
 $\int_a^b c \cdot s = c \int_a^b s$.
 
-\note{This property mirrors the \nameref{sub:step-homogeneous-property}.}
+\begin{note}
+  This property mirrors the \nameref{sub:step-homogeneous-property}.
+\end{note}
 
 \begin{proof}
 
@@ -2509,7 +2521,9 @@ $\int_a^b c \cdot s = c \int_a^b s$.
 
 $\int_{a+c}^{b+c} s(x) \mathop{dx} = \int_a^b s(x + c) \mathop{dx}$.
 
-\note{This property mirrors \nameref{sub:step-invariance-under-translation}.}
+\begin{note}
+  This property mirrors \nameref{sub:step-invariance-under-translation}.
+\end{note}
 
 \begin{proof}
 
@@ -2547,7 +2561,9 @@ $\int_{a+c}^{b+c} s(x) \mathop{dx} = \int_a^b s(x + c) \mathop{dx}$.
 
 If $s(x) < t(x)$ for each $x$ in $[a, b]$, then $\int_a^b s < \int_a^b t$.
 
-\note{This property mirrors the \nameref{sub:step-comparison-theorem}.}
+\begin{note}
+  This property mirrors the \nameref{sub:step-comparison-theorem}.
+\end{note}
 
 \begin{proof}
 

Bookshelf/Enderton/Set.tex

@@ -255,9 +255,26 @@ A \textbf{linear ordering} on $A$ (also called a \textbf{total ordering} on $A$)
   \item $R$ is \nameref{ref:trichotomous}.
 \end{enumerate}
 
+\begin{note}
+  This definition does not agree with how Lean defines a linear order.
+
+  \vspace{6pt}
+  Trichotomy is equivalent to asymmetry and connectivity and asymmetry is
+  equivalent to antisymmetry and irreflexivity. Thus a linear order, as defined
+  by Enderton, is a binary relation with the following four properties:
+
+  \vspace{6pt}
+  \begin{enumerate}[(i)]
+    \item Irreflexivity
+    \item Antisymmetry
+    \item Connectivity (i.e. totality)
+    \item Transitivity
+  \end{enumerate}
+\end{note}
+
 \begin{definition}
 
-  \lean*{Mathlib/Init/Algebra/Classes}{IsLinearOrder}
+  \lean*{Mathlib/Init/Algebra/Classes}{IsStrictTotalOrder}
 
 \end{definition}
 
@@ -811,7 +828,9 @@ List all the members of $V_4$.
 
   There is no set to which every set belongs.
 
-  \note{This was revisited after reading Enderton's proof prior.}
+  \begin{note}
+    This was revisited after reading Enderton's proof prior.
+  \end{note}
 
 \end{theorem}
 
@@ -2670,8 +2689,10 @@ If not, then under what conditions does equality hold?
 
   \lean*{Mathlib/SetTheory/ZFC/Basic}{Set.prod}
 
-  \note{The above Lean proof is a definition (i.e. an axiom). It does not prove
+  \begin{note}
-    such a set's existence from first principles.}
+    The above Lean proof is a definition (i.e. an axiom). It does not prove
+    such a set's existence from first principles.
+  \end{note}
 
   Define $C = A \cup B$.
   Then for all $x \in A$ and for all $y \in B$, $x$ and $y$ are both in $C$.
@@ -3556,7 +3577,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 \section{Ordering Relations}%
 \hyperlabel{sec:ordering-relations}
 
-\subsection{\pending{Theorem 3R}}%
+\subsection{\verified{Theorem 3R}}%
 \hyperlabel{sub:theorem-3r}
 
 \begin{theorem}[3R]
@@ -3571,6 +3592,9 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3r}
+
   Suppose $R$ is a \nameref{ref:linear-ordering} on $A$.
 
   \paragraph{(i)}%
@@ -5545,20 +5569,23 @@ State precisely the "analogous results" mentioned in Theorem 3Q.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.43}}%
+\subsection{\verified{Exercise 3.43}}%
-\label{sub:exercise-3.43}
+\hyperlabel{sub:exercise-3.43}
 
 Assume that $R$ is a linear ordering on a set $A$.
 Show that $R^{-1}$ is also a linear ordering on $A$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_43}
+
   Assume that $R$ is a \nameref{ref:linear-ordering} on a set $A$.
   Then $R$ is \nameref{ref:transitive} and \nameref{ref:trichotomous}.
   We show that (i) $R^{-1}$ is transitive and (ii) $R^{-1}$ is trichotomous.
 
   \paragraph{(i)}%
-  \label{par:exercise-3.43-i}
+  \hyperlabel{par:exercise-3.43-i}
 
     Let $\pair{x, y}, \pair{y, z} \in R^{-1}$.
     By definition of the \nameref{ref:inverse} of a set,
@@ -5568,7 +5595,7 @@ Show that $R^{-1}$ is also a linear ordering on $A$.
     Thus $R^{-1}$ is transitive.
 
   \paragraph{(ii)}%
-  \label{par:exercise-3.43-ii}
+  \hyperlabel{par:exercise-3.43-ii}
 
     Let $x, y \in A$.
     Since $R$ is trichotomous on $A$, it follows that exactly one of the
@@ -5586,8 +5613,8 @@ Show that $R^{-1}$ is also a linear ordering on $A$.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.44}}%
+\subsection{\verified{Exercise 3.44}}%
-\label{sub:exercise-3.44}
+\hyperlabel{sub:exercise-3.44}
 
 Assume that $<$ is a linear ordering on a set $A$.
 Assume that $f \colon A \rightarrow A$ and that $f$ has the property that
@@ -5596,6 +5623,14 @@ Show that $f$ is one-to-one and that whenever $f(x) < f(y)$, then $x < y$.
 
 \begin{proof}
 
+  \statementpadding
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_44\_i}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_44\_ii}
+
   We show that (i) $f$ is one-to-one and (ii) whenever $f(x) < f(y)$, then
     $x < y$.
 
@@ -5670,8 +5705,8 @@ Show that $f$ is one-to-one and that whenever $f(x) < f(y)$, then $x < y$.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.45}}%
+\subsection{\verified{Exercise 3.45}}%
-\label{sub:exercise-3.45}
+\hyperlabel{sub:exercise-3.45}
 
 Assume that $<_A$ and $<_B$ are linear orderings on $A$ and $B$, respectively.
 Define the binary relation $<_L$ on the Cartesian product $A \times B$ by:
@@ -5683,6 +5718,9 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_45}
+
   We show that $<_L$ is (i) \nameref{ref:transitive} and (ii)
     \nameref{ref:trichotomous} on $A \times B$.
 
@@ -5736,7 +5774,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
     There are three cases we examine:
 
     \subparagraph{Case 1}%
-    \label{spar:exercise-3.45-ii-case-1}
+    \hyperlabel{spar:exercise-3.45-ii-case-1}
 
       Suppose $a_1 <_A a_2$.
       Then $\pair{a_1, b_1} <_L \pair{a_2, b_2}$.

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -4,6 +4,7 @@ import Bookshelf.Enderton.Set.Relation
 import Common.Logic.Basic
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Rel
+import Mathlib.Init.Algebra.Classes
 import Mathlib.Order.RelClasses
 import Mathlib.Tactic.CasesM
 
@@ -2167,4 +2168,174 @@ theorem exercise_3_41_a {Q : Set.Relation (ℝ × ℝ)}
 
 end Relation
 
+/-- #### Theorem 3R
+
+Let `R` be a linear ordering on `A`.
+
+(i) There is no `x` for which `xRx`.
+(ii) For distinct `x` and `y` in `A`, either `xRy` or `yRx`.
+-/
+theorem theorem_3r {R : Rel α α} (hR : IsStrictTotalOrder α R)
+  : (∀ x : α, ¬ R x x) ∧ (∀ x y : α, x ≠ y → R x y ∨ R y x) := by
+  apply And.intro
+  · exact hR.irrefl
+  · intro x y h
+    apply Or.elim (hR.trichotomous x y)
+    · intro h₁
+      left
+      exact h₁
+    · intro h₁
+      apply Or.elim h₁
+      · intro h₂
+        exact absurd h₂ h
+      · intro h₂
+        right
+        exact h₂
+
+/-- #### Exercise 3.43
+
+Assume that `R` is a linear ordering on a set `A`. Show that `R⁻¹` is also a
+linear ordering on `A`.
+-/
+theorem exercise_3_43 {R : Rel α α} (hR : IsStrictTotalOrder α R)
+  : IsStrictTotalOrder α R.inv := by
+  refine { trichotomous := ?_, irrefl := ?_, trans := ?_ }
+  · intro a b
+    unfold Rel.inv flip
+    apply Or.elim (hR.trichotomous a b)
+    · intro h; right; right; exact h
+    · intro h
+      apply Or.elim h
+      · intro h; right; left; exact h
+      · intro h; left; exact h
+  · intro x h
+    unfold Rel.inv flip at h
+    exact absurd h (hR.irrefl x)
+  · intro a b c hab hac
+    unfold Rel.inv flip at *
+    exact hR.trans c b a hac hab
+
+/-! #### Exercise 3.44
+
+Assume that `<` is a linear ordering on a set `A`. Assume that `f : A → A` and
+that `f` has the property that whenever `x < y`, then `f(x) < f(y)`. Show that
+`f` is one-to-one and that whenever `f(x) < f(y)`, then `x < y`.
+-/
+
+theorem exercise_3_44_i {R : Rel α α} (hR : IsStrictTotalOrder α R)
+  (f : α → α) (hf : ∀ x y, R x y → R (f x) (f y))
+  : Function.Injective f := by
+  unfold Function.Injective
+  intro x₁ x₂ hx
+  apply Or.elim (hR.trichotomous x₁ x₂)
+  · -- `x₁ < x₂`
+    intro hx₁
+    have nh := hf x₁ x₂ hx₁
+    rw [hx] at nh
+    exact absurd nh (hR.irrefl (f x₂))
+  · intro hx₁
+    apply Or.elim hx₁
+    · simp  -- `x₁ = x₂`
+    · -- `x₁ > x₂`
+      intro hx₂
+      have nh := hf x₂ x₁ hx₂
+      rw [← hx] at nh
+      exact absurd nh (hR.irrefl (f x₁))
+
+theorem exercise_3_44_ii {R : Rel α α} (hR : IsStrictTotalOrder α R)
+  (f : α → α) (hf : ∀ x y, R x y → R (f x) (f y))
+  : R (f x) (f y) → R x y := by
+  intro h
+  apply Or.elim (hR.trichotomous x y)
+  · simp  -- `x < y`
+  · intro h₁
+    apply Or.elim h₁
+    · -- `x = y`
+      intro h₂
+      rw [h₂] at h
+      exact absurd h (hR.irrefl (f y))
+    · -- `x > y`
+      intro h₂
+      have := hR.trans (f x) (f y) (f x) h (hf y x h₂)
+      exact absurd this (hR.irrefl (f x))
+
+/-- #### Exercise 3.45
+
+Assume that `<_A` and `<_B` are linear orderings on `A` and `B`, respectively.
+Define the binary relation `<_L` on the Cartesian product `A × B` by:
+```
+⟨a₁, b₁⟩ <_L ⟨a₂, b₂⟩ iff either a₁ <_A a₂ or (a₁ = a₂ ∧ b₁ <_B b₂).
+```
+Show that `<_L` is a linear ordering on `A × B`. (The relation `<_L` is called
+*lexicographic* ordering, being the ordering used in making dictionaries.)
+-/
+theorem exercise_3_45 {A : Rel α α} {B : Rel β β} {R : Rel (α × β) (α × β)}
+  (hA : IsStrictTotalOrder α A) (hB : IsStrictTotalOrder β B)
+  (hR : ∀ a₁ b₁ a₂ b₂, R (a₁, b₁) (a₂, b₂) ↔ A a₁ a₂ ∨ (a₁ = a₂ ∧ B b₁ b₂))
+  : IsStrictTotalOrder (α × β) R := by
+  refine { trichotomous := ?_, irrefl := ?_, trans := ?_ }
+  · intro (a₁, b₁) (a₂, b₂)
+    apply Or.elim (hA.trichotomous a₁ a₂)
+    · -- `a₁ <_A a₂`
+      intro ha
+      left
+      exact (hR a₁ b₁ a₂ b₂).mpr (Or.inl ha)
+    · intro ha
+      apply Or.elim ha
+      · -- `a₁ = a₂`
+        intro ha₁
+        apply Or.elim (hB.trichotomous b₁ b₂)
+        · -- `b₁ <_B b₂`
+          intro hb
+          left
+          exact (hR a₁ b₁ a₂ b₂).mpr (Or.inr ⟨ha₁, hb⟩)
+        · intro hb
+          apply Or.elim hb
+          · -- `b₁ = b₂`
+            intro hb₁
+            right; left
+            rw [ha₁, hb₁]
+          · -- `b₂ <_B b₁`
+            intro hb₁
+            right; right
+            exact (hR a₂ b₂ a₁ b₁).mpr (Or.inr ⟨ha₁.symm, hb₁⟩)
+      · -- `a₂ <_A a₁`
+        intro ha₁
+        right; right
+        exact (hR a₂ b₂ a₁ b₁).mpr (Or.inl ha₁)
+  · intro (a, b) h
+    have := (hR a b a b).mp h
+    apply Or.elim this
+    · intro ha₁
+      exact absurd ha₁ (hA.irrefl a)
+    · intro ⟨_, hb₁⟩
+      exact absurd hb₁ (hB.irrefl b)
+  · intro (a₁, b₁) (a₂, b₂) (a₃, b₃) h₁ h₂
+    have h₁' := (hR a₁ b₁ a₂ b₂).mp h₁
+    have h₂' := (hR a₂ b₂ a₃ b₃).mp h₂
+    apply Or.elim h₁'
+    · -- `a₁ <_A a₂`
+      intro ha₁
+      apply Or.elim h₂'
+      · -- `a₂ <_A a₃`
+        intro ha₂
+        have := hA.trans a₁ a₂ a₃ ha₁ ha₂
+        exact (hR a₁ b₁ a₃ b₃).mpr (Or.inl this)
+      · -- `a₂ = a₃ ∧ b₂ <_B b₃`
+        intro ha₂
+        rw [ha₂.left] at ha₁
+        exact (hR a₁ b₁ a₃ b₃).mpr (Or.inl ha₁)
+    · -- `a₁ = a₂ ∧ b₁ <_B b₂`
+      intro ha₁
+      apply Or.elim h₂'
+      · -- `a₂ <_A a₃`
+        intro ha₂
+        rw [← ha₁.left] at ha₂
+        exact (hR a₁ b₁ a₃ b₃).mpr (Or.inl ha₂)
+      · -- `a₂ = a₃ ∧ b₂ <_B b₃`
+        intro ⟨ha₂, hb₂⟩
+        rw [← ha₁.left] at ha₂
+        have := hB.trans b₁ b₂ b₃ ha₁.right hb₂
+        exact (hR a₁ b₁ a₃ b₃).mpr (Or.inr ⟨ha₂, this⟩)
+
 end Enderton.Set.Chapter_3

preamble.tex

@@ -83,8 +83,8 @@
       \end{minipage}}
   \end{center}}
 
-\newcommand{\note}[1]{\@admonition{Note:}{#1}}
+\NewEnviron{note}{\@admonition{NOTE:}{\BODY}}
-\newcommand{\todo}[1]{\@admonition{TODO:}{#1}}
+\NewEnviron{todo}{\@admonition{TODO:}{\BODY}}
 
 % ========================================
 % Statements