Enderton. Exercise 3.38.

Bookshelf/Enderton/Set.tex

@@ -112,7 +112,7 @@ There is a set having no members:
 \end{axiom}
 
 \section{\defined{Equivalence Class}}%
-\label{sec:equivalence-class}
+\label{ref:equivalence-class}
 
 The set $[x]_R$ is defined by $$[x]_R = \{t \mid xRt\}.$$
 If $R$ is an \nameref{ref:equivalence-relation} and $x \in fld R$, then $[x]_R$
@@ -3409,8 +3409,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+  \lean{Bookshelf/Enderton/Set/Relation}{Set.Relation.modEquiv\_partition}
-    {Enderton.Set.Chapter\_3.theorem\_3p}
 
   Let $\Pi = \{[x]_R \mid x \in A\}$.
   We show that (i) there are no empty sets in $\Pi$, (ii) no two different sets
@@ -5165,7 +5164,7 @@ Show that $R_\Pi$ is an equivalence relation on $A$.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.38}}%
+\subsection{\verified{Exercise 3.38}}%
 \label{sub:exercise-3.38}
 
 \nameref{sub:theorem-3p} shows that $A / R$ is a partition of $A$ whenever $R$
@@ -5175,26 +5174,90 @@ Show that if we start with the equivalence relation $R_\Pi$ of the preceding
 
 \begin{proof}
 
-  If $\Pi$ is empty, its trivial to see $A / R_\Pi$ is likewise empty.
+  \lean{Bookshelf/Enderton/Set/Relation}
-  Thus assume $\Pi$ is not empty.
+    {Enderton.Set.Chapter\_3.exercise\_3\_38}
-  Let $C \in \Pi$.
+
-  By definition of a \nameref{ref:partition}, $C$ is nonempty.
+  By definition,
-  Let $x \in C$.
+    \begin{equation}
-  By definition of a \nameref{ref:partition}, every member of $\Pi$ is disjoint
+      \label{sub:exercise-3.38-eq1}
-    from every other.
+      R_\Pi = \{ (x, y) \mid (\exists B \in \Pi)(x \in B \land y \in B) \}.
-  Thus
+    \end{equation}
-    \begin{align*}
+  We prove that $A / R_\Pi = \Pi$.
-      C
+  By the \nameref{ref:extensionality-axiom}, these two sets are equal when
-        & = \{t \mid (\exists B \in \Pi)(x \in B \land t \in B)\} \\
+    $$B \in A / R_\Pi \iff B \in \Pi.$$
-        & = \{t \mid x R_\Pi t\} & \textref{sub:exercise-3.37} \\
+  We prove both directions of this biconditional.
-        & = [x]_{R_\Pi}.
+
-    \end{align*}
+  \paragraph{($\Rightarrow$)}%
-  Therefore every member of $\Pi$ is of form $[x]_{R_\Pi}$ for some $x \in A$.
+
-  In other words, $$A / R_\Pi = \{[x]_{R_\Pi} \mid x \in A\} = \Pi.$$
+    Suppose $B \in A / R_\Pi$.
+    By \nameref{sub:exercise-3.37}, $R_\Pi$ is an equivalence class.
+    Then, by definition of a \nameref{ref:quotient-set},
+      $$A / R_\Pi = \{[x]_{R_\Pi} \mid x \in A\},$$
+      whose members are the \nameref{ref:equivalence-class}es.
+    Thus there exists some $x \in A$ such that $B = [x]_{R_\Pi}$.
+    By definition of a \nameref{ref:partition}, there exists a unique set
+      $B' \in \Pi$ containing $x$.
+    Thus it suffices to prove that $B = B'$, for then $B = [x]_{R_\Pi} = B'$ is
+      a member of $\Pi$ as desired.
+    We proceed by extensionality again; that is, we show
+      $$y \in B \iff y \in B'.$$
+
+    \subparagraph{($\rightarrow$)}%
+
+      Suppose $y \in B$.
+      Then
+        \begin{align*}
+          y
+            & \in B = [x]_{R_\Pi} \\
+            & = \{t \mid \pair{x, t} \in R_\Pi\} \\
+            & = \{t \mid (\exists B_1 \in \Pi)(x \in B_1 \land t \in B_1)\}.
+              & \eqref{sub:exercise-3.38-eq1}
+        \end{align*}
+      Thus there exists some $B_1 \in \Pi$ such that $x \in B_1$ and
+        $y \in B_1$.
+      By definition of a \nameref{ref:partition}, $B_1 \in \Pi$ is the unique
+        member of $\Pi$ containing $y$.
+      Thus $B_1 = B'$ meaning $y \in B'$ as desired.
+
+    \subparagraph{($\leftarrow$)}%
+
+      Suppose $y \in B'$.
+      By construction, $x \in B'$.
+      Then there exists a set $B_1$ such that $x \in B_1$ and $y \in B_1$,
+        namely $B'$.
+      Therefore
+        \begin{align*}
+          y
+            & \in \{t \mid (\exists B_1 \in \Pi)(x \in B_1 \land t \in B_1)\} \\
+            & = \{t \mid \pair{x, t} \in R_\Pi\} \\
+            & = [x]_{R_\Pi} = B.
+        \end{align*}
+
+    \subparagraph{Conclusion}%
+
+      By the \nameref{ref:extensionality-axiom}, it follows $B = B'$.
+      Since $B' \in P$, it also follows $B \in P$.
+
+  \paragraph{($\Leftarrow$)}%
+
+    Let $B \in \Pi$.
+    By definition of a \nameref{ref:partition}, $B$ is nonempty.
+    Let $x \in B$.
+    By definition of a set, $B = \{t \mid x \in B \land t \in B\}$.
+    By definition of a \nameref{ref:partition}, every member of $B$ must belong
+      to only $B$ (i.e. no other sets in the partition).
+    Thus we can equivalently write
+      \begin{align*}
+        B
+          & = \{t \mid (\exists B_1 \in \Pi)(x \in B_1 \land t \in B_1)\} \\
+          & = \{ t \mid \pair{x, t} \in R_\Pi \} \\
+          & = [x]_{R_\Pi}.
+      \end{align*}
+    Therefore $B \in A / R_{\Pi}$.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.39}}%
+\subsection{\sorry{Exercise 3.39}}%
 \label{sub:exercise-3.39}
 
 Assume that we start with an equivalence relation $R$ on $A$ and define $\Pi$ to
@@ -5203,22 +5266,7 @@ Show that $R_\Pi$, as defined in Exercise 37, is just $R$.
 
 \begin{proof}
 
-  If $\Pi$ is empty, it's trivial to show $R_\Pi$ is also empty.
+  TODO
-  Thus assume $\Pi$ is not empty.
-  Let $C \in \Pi = A / R$.
-  By definition of a \nameref{ref:partition}, $C$ is nonempty.
-  Let $x \in C$.
-  Thus
-    \begin{align*}
-      C
-        & = [x]_R & \textref{sub:theorem-3p} \\
-        & = \{t \mid xRt\} \\
-        & = \{t \mid (\exists B \in A / R)(x \in B \land t \in B)\} \\
-        & = \{t \mid (\exists B \in \Pi)(x \in B \land t \in B)\} \\
-        & = \{t \mid x R_\Pi t\}.
-    \end{align*}
-  Thus $\pair{x, y} \in R_\Pi$ if and only if $\pair{x, y} \in R$.
-  By the \nameref{ref:extensionality-axiom}, $R_\Pi = R$.
 
 \end{proof}
 

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -1702,58 +1702,6 @@ theorem theorem_3m {R : Set.Relation α}
     have := hS ht
     exact hT this ht
 
-/-- #### Theorem 3P
-
-Assume that `R` is an equivalence relation on `A`. Then the set
-`{[x]_R | x ∈ A}` of all equivalence classes is a partition of `P`.
--/
-theorem theorem_3p {R : Set.Relation α} {A : Set α} {P : Set (Set α)}
-  (hR : R.isEquivalence A) (hP : P = {neighborhood R x | x ∈ A})
-  : isPartition P A := by
-  refine ⟨?_, ?_, ?_, ?_⟩
-  · -- Every member is a subset of `A`.
-    intro p hp
-    rw [hP] at hp
-    simp only [Set.mem_setOf_eq] at hp
-    have ⟨x, hx⟩ := hp
-    rw [← hx.right]
-    show ∀ t, t ∈ neighborhood R x → t ∈ A
-    intro t ht
-    exact hR.b_on (Or.inr (mem_pair_imp_snd_mem_ran ht))
-
-  · -- Every member is nonempty.
-    intro p hp
-    rw [hP] at hp
-    have ⟨x, hx⟩ := hp
-    rw [← hx.right]
-    exact ⟨x, hR.refl x hx.left⟩
-
-  · -- Every pair of members is disjoint.
-    intro xR hxR yR hyR h
-    by_contra nh
-    have nh' : Set.Nonempty (xR ∩ yR) := by
-      rw [← Set.nmem_singleton_empty]
-      exact nh
-    have ⟨z, hz⟩ := nh'
-    rw [hP] at hxR hyR
-    have ⟨x, hx⟩ := hxR
-    have ⟨y, hy⟩ := hyR
-    rw [← hx.right, ← hy.right] at hz
-    unfold neighborhood at hz
-    simp only [Set.mem_inter_iff, Set.mem_setOf_eq] at hz
-    have hzy : (z, y) ∈ R := hR.symm hz.right
-    have hxy : (x, y) ∈ R := hR.trans hz.left hzy
-    have := (neighborhood_iff_mem hR hx.left hy.left).mpr hxy
-    rw [hx.right, hy.right] at this
-    exact absurd this h
-
-  · -- Every element of `A` is in `P`.
-    intro x hx
-    have := hR.refl x hx
-    refine ⟨neighborhood R x, ?_, this⟩
-    · rw [hP]
-      exact ⟨x, hx, rfl⟩
-
 /-- #### Exercise 3.32 (a)
 
 Show that `R` is symmetric **iff** `R⁻¹ ⊆ R`.
@@ -1980,26 +1928,27 @@ theorem exercise_3_36 {f : Set.HRelation α β}
 
 /-- #### Exercise 3.37
 
-Assume that `Π` is a partition of a set `A`. Define the relation `R` as follows:
+Assume that `Π` is a partition of a set `A`. Define the relation `Rₚ` as
+follows:
 ```
-xRy ↔ (∃ B ∈ Π)(x ∈ B ∧ y ∈ B).
+xRₚy ↔ (∃ B ∈ Π)(x ∈ B ∧ y ∈ B).
 ```
-Show that `R` is an equivalence relation on `A`. (This is a formalized version
+Show that `Rₚ` is an equivalence relation on `A`. (This is a formalized version
 of the discussion at the beginning of this section.)
 -/
 theorem exercise_3_37 {P : Set (Set α)} {A : Set α}
-  (hP : isPartition P A) (R : Set.Relation α)
+  (hP : isPartition P A) (Rₚ : Set.Relation α)
-  (hR : ∀ x y, (x, y) ∈ R ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B)
+  (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B)
-  : isEquivalence R A := by
+  : isEquivalence Rₚ A := by
-  have hR' : R = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
+  have hR : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
     ext p
     have (x, y) := p
-    exact hR x y
+    exact hRₚ x y
-  refine ⟨?_, ?_, ?_, ?_⟩
 
-  · -- `fld R ⊆ A`
+  refine ⟨?_, ?_, ?_, ?_⟩
-    show ∀ x, x ∈ fld R → x ∈ A
+  · -- `fld Rₚ ⊆ A`
-    rw [hR']
+    show ∀ x, x ∈ fld Rₚ → x ∈ A
+    rw [hR]
     intro x hx
     unfold fld dom ran at hx
     simp only [
@@ -2018,25 +1967,25 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α}
       have := hP.p_subset B hB.left
       exact this hB.right.right
 
-  · -- `isReflexive R A`
+  · -- `isReflexive Rₚ A`
     intro x hx
-    rw [hR']
+    rw [hR]
     simp only [Set.mem_setOf_eq, and_self]
     exact hP.exhaustive x hx
 
-  · -- `isSymmetric R`
+  · -- `isSymmetric Rₚ`
     intro x y h
-    rw [hR'] at h
+    rw [hR] at h
     simp only [Set.mem_setOf_eq] at h
     have ⟨B, hB⟩ := h
-    rw [hR']
+    rw [hR]
     simp only [Set.mem_setOf_eq]
     conv at hB => right; rw [and_comm]
     exact ⟨B, hB⟩
 
-  · -- `isTransitive R`
+  · -- `isTransitive Rₚ`
     intro x y z hx hy
-    rw [hR'] at hx hy
+    rw [hR] at hx hy
     simp only [Set.mem_setOf_eq] at hx hy
     have ⟨B₁, hB₁⟩ := hx
     have ⟨B₂, hB₂⟩ := hy
@@ -2050,10 +1999,78 @@ 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]
     simp only [Set.mem_setOf_eq]
     exact ⟨B₁, hB₁.left, hB₁.right.left, by rw [hB]; exact hB₂.right.right⟩
 
+/-- #### Exercise 3.38
+
+Theorem 3P shows that `A / R` is a partition of `A` whenever `R` is an
+equivalence relation on `A`. Show that if we start with the equivalence relation
+`Rₚ` of the preceding exercise, then the partition `A / Rₚ` is just `P`.
+-/
+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
+    ext p
+    have (x, y) := p
+    exact hRₚ x y
+
+  ext B
+  apply Iff.intro
+  · intro ⟨x, hx⟩
+    have ⟨B', hB'⟩ := partition_mem_mem_eq hP hx.left
+    simp only at hB'
+    suffices B = B' by
+      rw [this]
+      exact hB'.left.left
+
+    ext y
+    apply Iff.intro
+    · intro hy
+      rw [← hx.right, hR] 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]
+      exact ⟨B', hB'.left.left, hB'.left.right, hy⟩
+
+  · intro hB
+    have ⟨x, hx⟩ := hP.nonempty B hB
+    have hx' : x ∈ A := hP.p_subset B hB hx
+    refine ⟨x, hx', Eq.symm ?_⟩
+    calc B
+      _ = {t | x ∈ B ∧ t ∈ B} := by
+        ext y
+        apply Iff.intro
+        · intro hy
+          exact ⟨hx, hy⟩
+        · intro hy
+          exact hy.right
+      _ = {t | ∃ B₁ ∈ P, x ∈ B₁ ∧ t ∈ B₁} := by
+        ext y
+        apply Iff.intro
+        · intro hy
+          exact ⟨B, hB, hy⟩
+        · intro hy
+          have ⟨B₁, hB₁⟩ := hy
+          have ⟨B', hB'⟩ := partition_mem_mem_eq hP hx'
+          simp only [Set.mem_setOf_eq] at *
+          have : B = B₁ := by
+            have lhs := hB'.right B ⟨hB, hx⟩
+            have rhs := hB'.right B₁ ⟨hB₁.left, hB₁.right.left⟩
+            rw [lhs, rhs]
+          rw [this]
+          exact hB₁.right
+      _ = {t | (x, t) ∈ Rₚ } := by
+        rw [hR]
+        simp only [Set.mem_setOf_eq]
+      _ = neighborhood Rₚ x := rfl
+
 end Relation
 
 end Enderton.Set.Chapter_3

Bookshelf/Enderton/Set/Relation.lean

@@ -529,6 +529,14 @@ and the members of the set. It isn't standard in anyway.
 -/
 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 : α}
+  (hR : isEquivalence R A) (hx : x ∈ A)
+  : x ∈ neighborhood R x := hR.refl x hx
+
 /--
 Assume that `R` is an equivalence relation on `A` and that `x` and `y` belong
 to `A`. Then `[x]_R = [y]_R ↔ xRy`.
@@ -560,6 +568,21 @@ structure isPartition (P : Set (Set α)) (A : Set α) : Prop where
   disjoint : ∀ a ∈ P, ∀ b, b ∈ P → a ≠ b → a ∩ b = ∅
   exhaustive : ∀ a ∈ A, ∃ p, p ∈ P ∧ a ∈ p
 
+/--
+Membership of sets within `P` is unique.
+-/
+theorem partition_mem_mem_eq {P : Set (Set α)} {A : Set α}
+  (hP : isPartition P A) (hx : x ∈ A)
+  : ∃! B, B ∈ P ∧ x ∈ B := by
+  have ⟨B, hB⟩ := hP.exhaustive x hx
+  refine ⟨B, hB, ?_⟩
+  intro B₁ hB₁
+  by_contra nB
+  have hB_disj := hP.disjoint B hB.left B₁ hB₁.left (Ne.symm nB)
+  rw [Set.ext_iff] at hB_disj
+  have := (hB_disj x).mp ⟨hB.right, hB₁.right⟩
+  simp at this
+
 /--
 The partition `A / R` induced by an equivalence relation `R`.
 -/