Enderton. Finish most equivalence class exercises.

Bookshelf/Enderton/Set.tex

@@ -3446,7 +3446,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \end{proof}
 
-\subsection{\pending{Theorem 3Q}}%
+\subsection{\unverified{Theorem 3Q}}%
 \hyperlabel{sub:theorem-3q}
 
 \begin{theorem}[3Q]
@@ -3480,7 +3480,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
   Since $F$ is compatible, $F(x_1)RF(x_2)$.
   Another application of \nameref{sub:lemma-3n} implies that
     $[F(x_1)]_R = [F(x_2)]_R$.
-  Thus $\hat{F}$ is be single-valued.
+  Thus $\hat{F}$ is single-valued.
 
   Uniqueness follows immediately from the \nameref{ref:extensionality-axiom}.
 
@@ -3491,7 +3491,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
   By \nameref{sub:lemma-3n}, $[x]_R = [y]_R$.
   For the sake of contradiction, suppose a function $\hat{F}$ exists satisfying
     \eqref{sub:theorem-3q-eq1}.
-  Then $\hat{F}([x]_R) = \hat{F}([y]_R)$ and $[F(x)]_R = [F(y)]_R$.
+  Then $\hat{F}([x]_R) = \hat{F}([y]_R)$ meaning $[F(x)]_R = [F(y)]_R$.
   Then \nameref{sub:lemma-3n} implies $F(x)RF(y)$, a contradiction.
   Therefore our original hypothesis must be incorrect.
   That is, there is no function $\hat{F}$ satisfying \eqref{sub:theorem-3q-eq1}.
@@ -4777,10 +4777,22 @@ Assume that $F \colon \powerset{A} \rightarrow \powerset{A}$ and that $F$ has
 Define
   $$B = \bigcap\{X \subseteq A \mid F(X) \subseteq X\} \quad\text{and}\quad
     C = \bigcup\{X \subseteq A \mid X \subseteq F(X)\}.$$
-\begin{enumerate}[(a)]
+
-  \item Show that $F(B) = B$ and $F(C) = C$.
+\subsubsection{\sorry{Exercise 3.30 (a)}}%
-  \item Show that if $F(X) = X$, then $B \subseteq X \subseteq C$.
+\hyperlabel{ssub:exercise-3.30-a}
-\end{enumerate}
+
+Show that $F(B) = B$ and $F(C) = C$.
+
+\begin{proof}
+
+  TODO
+
+\end{proof}
+
+\subsubsection{\sorry{Exercise 3.30 (b)}}%
+\hyperlabel{ssub:exercise-3.30-b}
+
+Show that if $F(X) = X$, then $B \subseteq X \subseteq C$.
 
 \begin{proof}
 
@@ -5257,7 +5269,7 @@ Show that if we start with the equivalence relation $R_\Pi$ of the preceding
 
 \end{proof}
 
-\subsection{\sorry{Exercise 3.39}}%
+\subsection{\verified{Exercise 3.39}}%
 \hyperlabel{sub:exercise-3.39}
 
 Assume that we start with an equivalence relation $R$ on $A$ and define $\Pi$ to
@@ -5266,11 +5278,44 @@ Show that $R_\Pi$, as defined in Exercise 37, is just $R$.
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_39}
+
+  By definition,
+    \begin{equation}
+      \hyperlabel{sub:exercise-3.39-eq1}
+      R_\Pi = \{ (x, y) \mid (\exists B \in \Pi)(x \in B \land y \in B) \}.
+    \end{equation}
+  We prove that $R_\Pi = R$.
+  By the \nameref{ref:extensionality-axiom}, these two sets are equal when
+    $$(x, y) \in R_\Pi \iff (x, y) \in R.$$
+  We prove both directions of this biconditional.
+
+  \paragraph{($\Rightarrow$)}%
+
+    Let $(x, y) \in R_\Pi$.
+    By \eqref{sub:exercise-3.39-eq1}, there exists some $B \in \Pi$ such that
+      $x \in B$ and $y \in B$.
+    Since $\Pi = A / R = \{[x]_R \mid x \in A\}$, there must exist some
+      $z \in A$ such that $B = [z]_R$.
+    By definition of an \nameref{ref:equivalence-class}, $x \in [z]_R$ implies
+      that $zRx$ and $y \in [z]_R$ implies $zRy$.
+    Since $R$ is \nameref{ref:symmetric}, $xRz$.
+    Since $R$ is \nameref{ref:transitive}, $xRy$.
+
+  \paragraph{($\Leftarrow$)}%
+
+    Let $(x, y) \in R$.
+    By definition of an \nameref{ref:equivalence-class}, $x \in [x]_R$ and
+      $y \in [x]_R$.
+    Note also that $[x]_R \in A / R = \Pi$.
+    Thus there exists some $B \in \Pi$ such that $x \in B$ and $y \in B$, namely
+      $B = [x]_R$.
+    By \eqref{sub:exercise-3.39-eq1}, $(x, y) \in R_\Pi$.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.40}}%
+\subsection{\unverified{Exercise 3.40}}%
 \hyperlabel{sub:exercise-3.40}
 
 Define an equivalence relation $R$ on the set $P$ of positive integers by
@@ -5294,25 +5339,106 @@ Is there a function $f \colon P / R \rightarrow P / R$ such that
 
 \end{proof}
 
-\subsection{\sorry{Exercise 3.41}}%
+\subsection{\unverified{Exercise 3.41}}%
 \hyperlabel{sub:exercise-3.41}
 
 Let $\mathbb{R}$ be the set of real numbers and define the relation $Q$ on
   $\mathbb{R} \times \mathbb{R}$ by $\pair{u, v}Q\pair{x, y}$ iff
   $u + y = x + v$.
 
-\begin{enumerate}[(a)]
+\subsubsection{\verified{Exercise 3.41a}}%
-  \item Show that $Q$ is an equivalence relation on
+\hyperlabel{ssub:exercise-3.41-a}
-    $\mathbb{R} \times \mathbb{R}$.
-  \item Is there a function $G \colon (\mathbb{R} \times \mathbb{R}) / Q
-    \rightarrow (\mathbb{R} \times \mathbb{R}) / Q$ satisfying the equation
-    $$G([\pair{x, y}]_Q) = [\pair{x + 2y, y + 2x}]_Q?$$
 
-\end{enumerate}
+Show that $Q$ is an equivalence relation on $\mathbb{R} \times \mathbb{R}$.
 
 \begin{proof}
 
-  TODO
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_41\_a}
+
+  We show (i) $Q$ is \nameref{ref:reflexive} on $\mathbb{R} \times \mathbb{R}$,
+    (ii) $Q$ is \nameref{ref:symmetric}, and (iii) $Q$ is
+    \nameref{ref:transitive}.
+
+  \paragraph{(i)}%
+
+    Let $\pair{x, y} \in R \times R$.
+    Since $x + y = x + y$, it immediately follows $\pair{x, y}Q\pair{x, y}$.
+    Thus $Q$ is reflexive on $\mathbb{R}$.
+
+  \paragraph{(ii)}%
+
+    Let $\pair{\pair{u, v}, \pair{x, y}} \in Q$.
+    Then $u + y = x + v$.
+    Likewise, $x + v = u + y$.
+    This immediately implies that $\pair{\pair{x, y}, \pair{u, v}} \in Q$.
+    Thus $Q$ is symmetric.
+
+  \paragraph{(iii)}%
+
+    Let $\pair{\pair{u, v}, \pair{x, y}} \in Q$ and
+      $\pair{\pair{x, y}, \pair{a, b}} \in Q$.
+    Then $u + y = x + v$ and $x + b = a + y$.
+    Rearranging terms, we have $u - v = x - y$ and $x - y = a - b$.
+    Thus $u - v = a - b$.
+    Rearranging terms once more yields $u + b = a + v$.
+    Thus $\pair{\pair{u, v}, \pair{a, b}} \in Q$.
+    Therefore $Q$ is transitive.
+
+\end{proof}
+
+\subsubsection{\unverified{Exercise 3.41b}}%
+\hyperlabel{ssub:exercise-3.41-b}
+
+Is there a function $G \colon (\mathbb{R} \times \mathbb{R}) / Q
+  \rightarrow (\mathbb{R} \times \mathbb{R}) / Q$ satisfying the equation
+  \begin{equation}
+    \hyperlabel{ssub:exercise-3.41-b-eq1}
+    G([\pair{x, y}]_Q) = [\pair{x + 2y, y + 2x}]_Q?
+  \end{equation}
+
+\begin{proof}
+
+  Let $f \colon \mathbb{R} \times \mathbb{R}
+    \rightarrow \mathbb{R} \times \mathbb{R}$ be given by
+    $f(\pair{x, y}) = \pair{x + 2y, y + 2x}$.
+  We show (i) that $f$ is \nameref{ref:compatible} with $Q$ and then (ii)
+    there exists such a function satisfying \eqref{ssub:exercise-3.41-b-eq1}.
+
+  \paragraph{(i)}%
+  \hyperlabel{par:exercise-3.41-b-i}
+
+    Let $\pair{u, v}, \pair{x, y} \in \mathbb{R} \times \mathbb{R}$ such that
+      $\pair{u, v} Q \pair{x, y}$.
+    Thus
+      \begin{equation}
+        \hyperlabel{ssub:exercise-3.41-b-eq2}
+        u + y = x + v
+      \end{equation}
+    Next consider
+      \begin{align*}
+        f(\pair{u, v}) & = \pair{u + 2v, v + 2u}, \\
+        f(\pair{x, y}) & = \pair{x + 2y, y + 2x}.
+      \end{align*}
+    Then
+      \begin{align*}
+             u + y & = x + v \\
+        \iff 3u + 3y & = 3x + 3v \\
+        \iff (u + y) + (2u + 2y) & = (x + v) + (2x + 2v) \\
+        \iff (x + v) + (2u + 2y) & = (u + y) + (2x + 2v)
+          & \eqref{ssub:exercise-3.41-b-eq2} \\
+        \iff (x + 2y) + (v + 2u) & = (u + 2v) + (y + 2x) \\
+        \iff (u + 2v) + (y + 2x) & = (x + 2y) + (v + 2u).
+      \end{align*}
+    This last equality shows $f(\pair{u, v}) \,Q\, f(\pair{x, y})$.
+    Thus $f$ is compatible with $Q$.
+
+  \paragraph{(ii)}%
+
+    By \nameref{par:exercise-3.41-b-i} and \nameref{sub:theorem-3q}, there
+      exists a unique $G \colon (\mathbb{R} \times \mathbb{R}) / Q \rightarrow
+      (\mathbb{R} \times \mathbb{R}) / Q$ satisfying
+      \eqref{ssub:exercise-3.41-b-eq1}.
 
 \end{proof}
 

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -2,6 +2,7 @@ import Bookshelf.Enderton.Set.Chapter_2
 import Bookshelf.Enderton.Set.OrderedPair
 import Bookshelf.Enderton.Set.Relation
 import Common.Logic.Basic
+import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.CasesM
 
 /-! # Enderton.Set.Chapter_3
@@ -1928,7 +1929,7 @@ theorem exercise_3_36 {f : Set.HRelation α β}
 
 /-- #### Exercise 3.37
 
-Assume that `Π` is a partition of a set `A`. Define the relation `Rₚ` as
+Assume that `P` is a partition of a set `A`. Define the relation `Rₚ` as
 follows:
 ```
 xRₚy ↔ (∃ B ∈ Π)(x ∈ B ∧ y ∈ B).
@@ -1940,7 +1941,7 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α}
   (hP : isPartition P A) (Rₚ : Set.Relation α)
   (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B)
   : isEquivalence Rₚ A := by
-  have hR : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
+  have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
     ext p
     have (x, y) := p
     exact hRₚ x y
@@ -1948,7 +1949,7 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α}
   refine ⟨?_, ?_, ?_, ?_⟩
   · -- `fld Rₚ ⊆ A`
     show ∀ x, x ∈ fld Rₚ → x ∈ A
-    rw [hR]
+    rw [hRₚ_eq]
     intro x hx
     unfold fld dom ran at hx
     simp only [
@@ -1969,23 +1970,23 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α}
 
   · -- `isReflexive Rₚ A`
     intro x hx
-    rw [hR]
+    rw [hRₚ_eq]
     simp only [Set.mem_setOf_eq, and_self]
     exact hP.exhaustive x hx
 
   · -- `isSymmetric Rₚ`
     intro x y h
-    rw [hR] at h
+    rw [hRₚ_eq] at h
     simp only [Set.mem_setOf_eq] at h
     have ⟨B, hB⟩ := h
-    rw [hR]
+    rw [hRₚ_eq]
     simp only [Set.mem_setOf_eq]
     conv at hB => right; rw [and_comm]
     exact ⟨B, hB⟩
 
   · -- `isTransitive Rₚ`
     intro x y z hx hy
-    rw [hR] at hx hy
+    rw [hRₚ_eq] at hx hy
     simp only [Set.mem_setOf_eq] at hx hy
     have ⟨B₁, hB₁⟩ := hx
     have ⟨B₂, hB₂⟩ := hy
@@ -1999,7 +2000,7 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α}
       intro h'
       rw [Set.ext_iff] at h'
       exact (h' y).mp ⟨hy₁, hy₂⟩
-    rw [hR]
+    rw [hRₚ_eq]
     simp only [Set.mem_setOf_eq]
     exact ⟨B₁, hB₁.left, hB₁.right.left, by rw [hB]; exact hB₂.right.right⟩
 
@@ -2013,7 +2014,7 @@ theorem exercise_3_38 {P : Set (Set α)} {A : Set α}
   (hP : isPartition P A) (Rₚ : Set.Relation α)
   (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B)
   : modEquiv (exercise_3_37 hP Rₚ hRₚ) = P := by
-  have hR : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
+  have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
     ext p
     have (x, y) := p
     exact hRₚ x y
@@ -2030,13 +2031,13 @@ theorem exercise_3_38 {P : Set (Set α)} {A : Set α}
     ext y
     apply Iff.intro
     · intro hy
-      rw [← hx.right, hR] at hy
+      rw [← hx.right, hRₚ_eq] at hy
       have ⟨B₁, hB₁⟩ := hy
       have := hB'.right B₁ ⟨hB₁.left, hB₁.right.left⟩
       rw [← this]
       exact hB₁.right.right
     · intro hy
-      rw [← hx.right, hR]
+      rw [← hx.right, hRₚ_eq]
       exact ⟨B', hB'.left.left, hB'.left.right, hy⟩
 
   · intro hB
@@ -2067,10 +2068,101 @@ theorem exercise_3_38 {P : Set (Set α)} {A : Set α}
           rw [this]
           exact hB₁.right
       _ = {t | (x, t) ∈ Rₚ } := by
-        rw [hR]
+        rw [hRₚ_eq]
         simp only [Set.mem_setOf_eq]
       _ = neighborhood Rₚ x := rfl
 
+/-- #### Exercise 3.39
+
+Assume that we start with an equivalence relation `R` on `A` and define `P` to
+be the partition `A / R`. Show that `Rₚ`, as defined in Exercise 37, is just
+`R`.
+-/
+theorem exercise_3_39 {P : Set (Set α)} {R Rₚ : Set.Relation α} {A : Set α}
+  (hR : isEquivalence R A) (hP : P = modEquiv hR)
+  (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B)
+  : Rₚ = R := by
+  have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
+    ext p
+    have (x, y) := p
+    exact hRₚ x y
+
+  ext p
+  have (x, y) := p
+  apply Iff.intro
+  · intro hp
+    rw [hRₚ_eq] at hp
+    have ⟨B, hB, hx, hy⟩ := hp
+    rw [hP] at hB
+    have ⟨z, hz⟩ := hB
+    rw [← hz.right] at hx hy
+    exact neighborhood_mem_imp_relate hR hx hy
+  · intro hp
+    have hxA : x ∈ A := hR.b_on (Or.inl (mem_pair_imp_fst_mem_dom hp))
+    have hyA : y ∈ A := hR.b_on (Or.inr (mem_pair_imp_snd_mem_ran hp))
+    rw [hRₚ_eq]
+    have hx : x ∈ neighborhood R x := neighborhood_self_mem hR hxA
+    have hy : y ∈ neighborhood R x := by
+      rw [← neighborhood_eq_iff_mem_relate hR hxA hyA] at hp
+      rw [hp]
+      exact neighborhood_self_mem hR hyA
+    refine ⟨neighborhood R x, ?_, ⟨hx, hy⟩⟩
+    rw [hP]
+    exact ⟨x, hxA, rfl⟩
+lemma test {x y z : ℝ} (h : x + y = z) : (x = z - y) := by apply?
+/-- #### Exercise 3.41 (a)
+
+Let `ℝ` be the set of real numbers and define the realtion `Q` on `ℝ × ℝ` by
+`⟨u, v⟩ Q ⟨x, y⟩` **iff** `u + y = x + v`. Show that `Q` is an equivalence
+relation on `ℝ × ℝ`.
+-/
+theorem exercise_3_41_a {Q : Set.Relation (ℝ × ℝ)}
+  (hQ : ∀ u v x y, ((u, v), (x, y)) ∈ Q ↔ u + y = x + v)
+  : isEquivalence Q (Set.univ : Set (ℝ × ℝ)) := by
+  have hQ_eq : Q = {p | p.1.1 + p.2.2 = p.2.1 + p.1.2} := by
+    ext p
+    apply Iff.intro <;>
+    · intro hp
+      rwa [hQ] at *
+
+  refine ⟨?_, ?_, ?_, ?_⟩
+
+  · -- `fld Q ⊆ Set.univ`
+    show ∀ p, p ∈ fld Q → p ∈ Set.univ
+    intro _ _
+    simp only [Set.mem_univ]
+
+  · -- `isReflexive Q Set.univ`
+    intro (x, y) _
+    rw [hQ_eq]
+    simp
+
+  · -- `isSymmetric Q`
+    intro (u, v) (x, y) hp
+    rw [hQ_eq] at *
+    exact Eq.symm hp
+
+  · -- `isTransitive Q`
+    unfold isTransitive
+    intro (u, v) (x, y) (a, b) h₁ h₂
+    rw [hQ_eq] at *
+    simp at h₁ h₂
+    simp
+    have h₁' : u - v = x - y := by
+      have := sub_eq_of_eq_add h₁
+      rw [add_sub_right_comm] at this
+      exact eq_sub_of_add_eq this
+    have h₂' : x - y = a - b := by
+      have := sub_eq_of_eq_add h₂
+      rw [add_sub_right_comm] at this
+      exact eq_sub_of_add_eq this
+    rw [h₂'] at h₁'
+    have := eq_add_of_sub_eq' h₁'
+    rw [← add_sub_assoc] at this
+    have := add_eq_of_eq_sub this
+    conv => right; rw [add_comm]
+    exact this
+
 end Relation
 
 end Enderton.Set.Chapter_3

Bookshelf/Enderton/Set/Relation.lean

@@ -533,7 +533,7 @@ def neighborhood (R : Relation α) (x : α) := { t | (x, t) ∈ R }
 The neighborhood with some respect to an equivalence relation `R` on set `A`
 and member `x` contains `x`.
 -/
-theorem neighborhood_self_mem {R : Set.Relation α} {A : Set α} {x : α}
+theorem neighborhood_self_mem {R : Set.Relation α} {A : Set α}
   (hR : isEquivalence R A) (hx : x ∈ A)
   : x ∈ neighborhood R x := hR.refl x hx
 
@@ -541,7 +541,7 @@ theorem neighborhood_self_mem {R : Set.Relation α} {A : Set α} {x : α}
 Assume that `R` is an equivalence relation on `A` and that `x` and `y` belong
 to `A`. Then `[x]_R = [y]_R ↔ xRy`.
 -/
-theorem neighborhood_iff_mem {R : Set.Relation α} {A : Set α} {x y : α}
+theorem neighborhood_eq_iff_mem_relate {R : Set.Relation α} {A : Set α}
   (hR : isEquivalence R A) (_ : x ∈ A) (hy : y ∈ A)
   : neighborhood R x = neighborhood R y ↔ (x, y) ∈ R := by
   apply Iff.intro
@@ -558,6 +558,19 @@ theorem neighborhood_iff_mem {R : Set.Relation α} {A : Set α} {x y : α}
     · intro ht
       exact hR.trans h ht
 
+/--
+Assume that `R` is an equivalence relation on `A`. If two sets `x` and `y`
+belong to the same neighborhood, then `xRy`. 
+-/
+theorem neighborhood_mem_imp_relate {R : Set.Relation α} {A : Set α}
+  (hR : isEquivalence R A)
+  (hx : x ∈ neighborhood R z) (hy : y ∈ neighborhood R z)
+  : (x, y) ∈ R := by
+  unfold neighborhood at hx hy
+  simp only [mem_setOf_eq] at hx hy
+  have := hR.symm hx
+  exact hR.trans this hy
+
 /--
 A **partition** `Π` of a set `A` is a set of nonempty subsets of `A` that is
 disjoint and exhaustive.
@@ -622,8 +635,8 @@ theorem modEquiv_partition {A : Set α} {R : Relation α} (hR : isEquivalence R
       have : z ∈ fld R := Or.inr (mem_pair_imp_snd_mem_ran hz.left)
       exact hR.b_on this
     rw [
-      ← neighborhood_iff_mem hR hx.left hz_mem,
+      ← neighborhood_eq_iff_mem_relate hR hx.left hz_mem,
-      ← neighborhood_iff_mem hR hy.left hz_mem,
+      ← neighborhood_eq_iff_mem_relate hR hy.left hz_mem,
       hx.right, hy.right
     ] at hz
     rw [hz.left, hz.right] at nXY