Enderton (set). Work through backlog of theorems and exercises.

Bookshelf/Enderton/Set.tex

@@ -3083,7 +3083,7 @@
       \end{align*}
   \end{proof}
 
-\subsection{\pending{Theorem 3J}}%
+\subsection{\verified{Theorem 3J}}%
 \hyperlabel{sub:theorem-3j}
 
   \begin{theorem}[3J]
@@ -3098,6 +3098,12 @@
     \end{enumerate}
   \end{theorem}
 
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3j\_a}
+
+  \code{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3j\_b}
+
   \begin{proof}
     Let $F$ be a \nameref{ref:function} from nonempty set $A$ to set $B$.
 
@@ -3577,7 +3583,11 @@
       $$\hat{F} = \{\tuple{[x]_R, [F(x)]_R} \mid x \in A\}.$$
     By construction $\hat{F}$ has domain $A / R$ and
       $\ran{\hat{F}} \subseteq A / R$.
-    All that remains is proving $\hat{F}$ is single-valued.
+    All that remains is proving (i) $\hat{F}$ is single-valued and (ii)
+      $\hat{F}$ is unique.
+
+    \paragraph{(i)}%
+
       Let $[x_1]_R, [x_2]_R \in \dom{\hat{F}}$ such that $[x_1]_R = [x_2]_R$.
       By definition of $\hat{F}$, $\tuple{[x_1]_R, [F(x_1)]_R} \in \hat{F}$
         and $\tuple{[x_2]_R, [F(x_2)]_R} \in \hat{F}$.
@@ -3585,12 +3595,23 @@
       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 single-valued.
+      Thus $\hat{F}$ is single-valued, i.e. a function.
 
-    Uniqueness follows immediately from the \nameref{ref:extensionality-axiom}.
+    \paragraph{(ii)}%
+
+      Suppose there exists another function, say $\hat{G}$, that satisfies
+        \eqref{sub:theorem-3q-eq1}.
+      That is,
+        $$\hat{G}([x]_R) = [F(x)]_R \quad\text{for all } x \text{ in } A.$$
+      Let $x \in A$.
+      Then $\hat{G}([x]_R) = [F(x)]_R$ and $\hat{F}([x]_R) = [F(x)]_R$.
+      Since this holds for all $x \in A$, $\hat{F}$ and $\hat{G}$ agree on all
+        equivalence classes in $A / R$.
+      Hence, by the \nameref{ref:extensionality-axiom}, $\hat{F} = \hat{G}$.
 
     \suitdivider
 
+    \noindent
     Suppose $F$ is not compatible with $R$.
     Then there exists some $x, y \in A$ such that $xRy$ and $\neg F(x)RF(y)$.
     By \nameref{sub:lemma-3n}, $[x]_R = [y]_R$.
@@ -3599,7 +3620,7 @@
     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
+    That is, there is no incompatible function $\hat{F}$ satisfying
       \eqref{sub:theorem-3q-eq1}.
   \end{proof}
 
@@ -4808,7 +4829,7 @@
   Does the converse hold?
 
   \code*{Bookshelf/Enderton/Set/Chapter\_3}
-    {Enderton.Set.Chapter\_3.exercise\_3\_39}
+    {Enderton.Set.Chapter\_3.exercise\_3\_29}
 
   \begin{proof}
     Let $f \colon A \rightarrow B$ such that $f$ maps $A$ onto $B$.
@@ -4847,7 +4868,7 @@
       corresponds to value $2$.
   \end{proof}
 
-\subsection{\sorry{Exercise 3.30}}%
+\subsection{\verified{Exercise 3.30}}%
 \hyperlabel{sub:exercise-3.30}
 
   Assume that $F \colon \powerset{A} \rightarrow \powerset{A}$ and that $F$ has
@@ -4857,22 +4878,89 @@
     $$B = \bigcap\{X \subseteq A \mid F(X) \subseteq X\} \quad\text{and}\quad
       C = \bigcup\{X \subseteq A \mid X \subseteq F(X)\}.$$
 
-\subsubsection{\sorry{Exercise 3.30 (a)}}%
+\subsubsection{\verified{Exercise 3.30 (a)}}%
 \hyperlabel{ssub:exercise-3.30-a}
 
   Show that $F(B) = B$ and $F(C) = C$.
 
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_30\_a}
+
   \begin{proof}
-    TODO
+
+    We prove that (i) $F(B) = B$ and (ii) $F(C) = C$.
+
+    \paragraph{(i)}%
+    \hyperlabel{par:exercise-3.30-a-i}
+
+      To prove $F(B) = B$, we show $F(B) \subseteq B$ and $F(B) \supseteq B$.
+
+      \subparagraph{($\subseteq$)}%
+      \hyperlabel{spar:exercise-3.30-i-sub}
+
+        Let $x \in F(B)$ and $X \subseteq A$ such that $F(X) \subseteq X$.
+        By definition of $B$, $B \subseteq X$.
+        Then monotonicity implies $F(B) \subseteq F(X) \subseteq X$.
+        Therefore $x \in X$.
+        Since $X$ was arbitrarily chosen, it follows that
+          $$\forall X, X \subseteq A \land F(X) \subseteq X \Rightarrow
+            x \in X.$$
+        By definition of the intersection of sets,
+          $$x \in \bigcap\{X \subseteq A \mid F(X) \subseteq X\} = B.$$
+        Hence $F(B) \subseteq B$.
+
+      \subparagraph{($\supseteq$)}%
+
+        By \nameref{spar:exercise-3.30-i-sub}, $F(B) \subseteq B$.
+        Then monotonicity implies $F(F(B)) \subseteq F(B)$.
+        Thus $F(B) \in \{X \subseteq A \mid F(X) \subseteq X\}$.
+        Hence, by definition of $B$, $B \subseteq F(B)$.
+
+    \paragraph{(ii)}%
+
+      To prove $F(C) = C$, we show $F(C) \supseteq C$ and $F(C) \subseteq C$.
+
+      \subparagraph{($\supseteq$)}%
+      \hyperlabel{spar:exercise-3.30-i-sup}
+
+        Let $x \in C$.
+        By definition of $C$, there exists some $X \subseteq A$ such that
+          $X \subseteq F(X)$ and $x \in X$.
+        Since $C$ contains $X$, $X \subseteq C$.
+        Then monotonicity implies $X \subseteq F(X) \subseteq F(C)$.
+        Therefore $x \in F(C)$.
+
+      \subparagraph{($\subseteq$)}%
+
+        By \nameref{spar:exercise-3.30-i-sup}, $C \subseteq F(C)$.
+        Then monotonicity implies $F(C) \subseteq F(F(C))$.
+        Thus $F(C) \in \{X \subseteq A \mid X \subseteq F(X)\}$.
+        Hence, by definition of $C$, $F(C) \subseteq C$.
+
   \end{proof}
 
-\subsubsection{\sorry{Exercise 3.30 (b)}}%
+\subsubsection{\verified{Exercise 3.30 (b)}}%
 \hyperlabel{ssub:exercise-3.30-b}
 
   Show that if $F(X) = X$, then $B \subseteq X \subseteq C$.
 
+  \code*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_30\_b}
+
   \begin{proof}
-    TODO
+    Suppose $F(X) = X$ for some $X \subseteq A$.
+    By the \nameref{ref:extensionality-axiom}, $F(X) \subseteq X$ and
+      $X \subseteq F(X)$.
+    Therefore
+      \begin{align}
+        X & \in \{X \subseteq A \mid F(X) \subseteq X\}
+          & \hyperlabel{ssub:exercise-3.30-b-eq1} \\
+        X & \in \{X \subseteq A \mid X \subseteq F(X)\}.
+          & \hyperlabel{ssub:exercise-3.30-b-eq2}
+      \end{align}
+    \eqref{ssub:exercise-3.30-b-eq1} immediately implies $B \subseteq X$ and
+      \eqref{ssub:exercise-3.30-b-eq2} immediately implies $X \subseteq C$.
+    Thus $B \subseteq X \subseteq C$.
   \end{proof}
 
 \subsection{\unverified{Exercise 3.31}}%
@@ -5502,14 +5590,93 @@
 
   \end{proof}
 
-\subsection{\sorry{Exercise 3.42}}%
+\subsection{\unverified{Exercise 3.42}}%
 \hyperlabel{sub:exercise-3.42}
 
-  State precisely the "analogous results" mentioned in Theorem 3Q.
+  State precisely the "analogous results" mentioned in \nameref{sub:theorem-3q}.
   (This will require extending the concept of compatibility in a suitable way.)
 
+  \linedivider
+
+  \begin{theorem}[3.42]
+    A function $F \colon A \times A \rightarrow A$ is said to be
+      \textbf{compatible} with relation $R$ if and only if for all
+      $x_1, y_1, x_2, y_2 \in A$,
+      $$x_1Rx_2 \land y_1Ry_2 \Rightarrow F(x_1, y_1)RF(x_2, y_2).$$
+
+    \noindent
+    Assume that $R$ is an equivalence relation on $A$ and that
+      $F \colon A \times A \rightarrow A$.
+    If $F$ is compatible with $R$, then there exists a unique function
+      $\hat{F} \colon A / R \times A / R \rightarrow A / R$ such that
+      \begin{equation}
+        \hyperlabel{sub:exercise-3.42-eq1}
+        \hat{F}([x]_R, [y]_R) = [F(x, y)]_R
+      \end{equation}
+      for all $x, y \in A$.
+    If $F$ is not compatible with $R$, then no such $\hat{F}$ exists.
+  \end{theorem}
+
   \begin{proof}
-    TODO
+    Let $R$ be an equivalence relation on $A$ and
+      $F \colon A \times A \rightarrow A$ be compatible with $R$.
+    Define relation $\hat{F}$ to be
+      $$\hat{F} = \{\tuple{[x]_R, [y]_R, [F(x, y)]_R} \mid x, y \in A\}.$$
+    By construction, $\dom{\hat{F}} = A / R \times A / R$ and
+      $\ran{\hat{F}} \subseteq A / R$.
+    All that remains is proving (i) $\hat{F}$ is single-valued and (ii)
+      $\hat{F}$ is unique.
+
+    \paragraph{(i)}%
+
+      Let $[x_1]_R, [y_1]_R, [x_2]_R, [y_2]_R \in \dom{\hat{F}}$ such that
+        \begin{equation}
+          \hyperlabel{par:theorem-3q-i-eq1}
+          \tuple{[x_1]_R, [y_1]_R} = \tuple{[x_2]_R, [y_2]_R}.
+        \end{equation}
+      By definition of $\hat{F}$,
+        \begin{align*}
+          \tuple{[x_1]_R, [y_1]_R, [F(x_1, y_1)]_R} & \in \hat{F} \\
+          \tuple{[x_2]_R, [y_2]_R, [F(x_2, y_2)]_R} & \in \hat{F}.
+        \end{align*}
+      By \eqref{par:theorem-3q-i-eq1}, $[x_1]_R = [x_2]_R$ and
+        $[y_1]_R = [y_2]_R$.
+      Then \nameref{sub:lemma-3n} implies $x_1Rx_2$ and $y_1Ry_2$ respectively.
+      Since $F$ is compatible, it follows $F(x_1, y_1)RF(x_2, y_2)$.
+      Another application of \nameref{sub:lemma-3n} implies that
+        $[F(x_1, y_1)]_R = [F(x_2, y_2)]_R$.
+      Thus $\hat{F}$ is single-valued, i.e. a function.
+
+    \paragraph{(ii)}%
+
+      Suppose there exists another function, say $\hat{G}$, that satisfies
+        \eqref{sub:exercise-3.42-eq1}.
+      That is,
+        $$\hat{G}([x]_R, [y]_R) = [F(x, y)]_R \quad\text{for all } x, y \in A.$$
+      Let $x, y \in A$.
+      Then $\hat{G}([x]_R, [y]_R) = [F(x, y)]_R$ and
+        $\hat{F}([x]_R, [y]_R) = [F(x, y)]_R$.
+      Since this holds for all $x, y \in A$, $\hat{F}$ and $\hat{G}$ agree on
+        all members of $A / R \times A / R$.
+      Hence, by the \nameref{ref:extensionality-axiom}, $\hat{F} = \hat{G}$.
+
+    \suitdivider
+
+    \noindent
+    Suppose $F$ is not compatible with $R$.
+    Then there exists some $x_1, y_1, x_2, y_2 \in A$ such that $x_1Rx_2$ and
+      $y_1Ry_2$ but $\neg F(x_1, y_1)RF(x_2, y_2)$.
+    By \nameref{sub:lemma-3n}, $[x_1]_R = [x_2]_R$ and $[y_1]_R = [y_2]_R$.
+    For the sake of contradiction, suppose a function $\hat{F}$ exists
+      satisfying \eqref{sub:exercise-3.42-eq1}.
+    Then $\hat{F}([x_1]_R, [y_1]_R) = \hat{F}([x_2]_R, [y_2]_R)$ meaning
+      $[F(x_1, y_1)]_R = [F(x_2, y_2)]_R$.
+    Then \nameref{sub:lemma-3n} implies $F(x_1, y_1)RF(x_2, y_2)$, a
+      contradiction.
+    Therefore our original hypothesis must be incorrect.
+    That is, there is no incompatible function $\hat{F}$ satisfying
+      \eqref{sub:exercise-3.42-eq1}.
+
   \end{proof}
 
 \subsection{\verified{Exercise 3.43}}%

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -114,32 +114,152 @@ Assume that `F : A → B`, and that `A` is nonempty. There exists a function
 `G : B → A` (a "left inverse") such that `G ∘ F` is the identity function on `A`
 **iff** `F` is one-to-one.
 -/
-theorem theorem_3j_a {F : Set.HRelation α β} {A : Set α} {B : Set β}
+theorem theorem_3j_a {F : Set.HRelation α β}
   (hF : mapsInto F A B) (hA : Set.Nonempty A)
-  : (∃ G : Set.HRelation β α,
+  : isOneToOne F ↔
-      mapsInto G B A ∧
+      ∃ G, mapsInto G B A ∧ comp G F = { p | p.1 ∈ A ∧ p.1 = p.2 } := by
-        (comp G F = { p | p.1 ∈ A ∧ p.1 = p.2 })) ↔ isOneToOne F := by
   apply Iff.intro
-  · intro ⟨G, hG⟩
+  · intro h
+    have ⟨a, ha⟩ := hA
+    -- `G(y) = if y ∈ ran F then F⁻¹(y) else a`
+    let G : Set.HRelation β α :=
+      restriction (inv F) B ∪ { p | p.1 ∈ B ∧ p.1 ∉ ran F ∧ p.2 = a }
+
+    refine ⟨G, ⟨?_, ?_, ?_⟩, ?_⟩
+    · show isSingleValued G
+      intro x hx
+      have ⟨y, hy⟩ := dom_exists hx
+      refine ⟨y, ⟨mem_pair_imp_snd_mem_ran hy, hy⟩, ?_⟩
+      intro y₁ hy₁
+      dsimp only at hy₁
+      apply Or.elim hy₁.right
+      · -- Supposes `y₁ ∈ ran F`.
+        intro hF_inv
+        unfold restriction at hF_inv
+        simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq] at hF_inv
+        dsimp only at hy
+        unfold restriction at hy
+        simp only [Set.mem_union, Set.mem_setOf_eq] at hy
+        apply Or.elim hy
+        · intro ⟨hz, _⟩
+          have : isOneToOne (inv F) := one_to_one_self_iff_one_to_one_inv.mp h
+          exact single_valued_eq_unique this.left hF_inv.left hz
+        · intro hz
+          rw [hz.right.right]
+          simp only [mem_self_comm_mem_inv] at hF_inv
+          have := mem_pair_imp_snd_mem_ran hF_inv.left
+          exact absurd this hz.right.left
+      · -- Supposes `y₁ ∉ ran F`.
+        intro hF_id
+        simp at hF_id
+        dsimp only at hy
+        unfold restriction at hy
+        simp at hy
+        apply Or.elim hy
+        · intro hz
+          have := mem_pair_imp_snd_mem_ran hz.left
+          exact absurd this hF_id.right.left
+        · intro hz
+          rw [hF_id.right.right, hz.right.right]
+
+    · show dom G = B
+      ext b
+      unfold dom Prod.fst Set.image
+      simp only [
+        Set.mem_union,
+        Set.mem_setOf_eq,
+        Prod.exists,
+        exists_and_right,
+        exists_eq_right
+      ]
+      apply Iff.intro
+      · intro ⟨x, hx⟩
+        apply Or.elim hx (fun hb => hb.right) (fun hb => hb.left)
+      · intro hb
+        by_cases hb' : b ∈ ran F
+        · have ⟨t, ht⟩ := ran_exists hb'
+          refine ⟨t, ?_⟩
+          left
+          unfold restriction inv
+          simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq]
+          exact ⟨⟨t, b, ht, rfl, rfl⟩, hb⟩
+        · refine ⟨a, ?_⟩
+          right
+          exact ⟨hb, hb', rfl⟩
+
+    · show ∀ t, t ∈ ran G → t ∈ A  -- `ran G ⊆ A`
+      intro t ht
+      dsimp only at ht
+      unfold ran Prod.snd restriction inv at ht
+      simp only [
+        Prod.exists,
+        Set.mem_setOf_eq,
+        Set.mem_image,
+        exists_eq_right,
+        not_exists,
+        Set.mem_union,
+        Prod.mk.injEq
+      ] at ht
+      have ⟨a₁, ha₁⟩ := ht 
+      apply Or.elim ha₁
+      · intro ⟨⟨a, b, hab⟩, _⟩
+        have := mem_pair_imp_fst_mem_dom hab.left
+        rwa [← hab.right.right, ← hF.dom_eq]
+      · intro h
+        rwa [h.right.right]
+
+    · -- Show that `G ∘ F` is the identity function on `A`.
+      show comp G F = {p | p.fst ∈ A ∧ p.fst = p.snd}
+      unfold comp
+      ext p
+      have (x, y) := p
+      simp only [Set.mem_union, Set.mem_setOf_eq]
+      apply Iff.intro
+      · intro ⟨t, hx, ht⟩
+        refine ⟨hF.dom_eq ▸ mem_pair_imp_fst_mem_dom hx, ?_⟩
+        apply Or.elim ht
+        · intro ht'
+          unfold restriction inv at ht'
+          simp at ht'
+          have ⟨c, d, hcd⟩ := ht'.left
+          rw [hcd.right.left, hcd.right.right] at hcd
+          exact single_rooted_eq_unique h.right hx hcd.left
+        · intro ht'
+          exact absurd (mem_pair_imp_snd_mem_ran hx) ht'.right.left
+      · intro hx
+        rw [← hF.dom_eq] at hx
+        have ⟨t, ht⟩ := dom_exists hx.left
+        refine ⟨t, ht, ?_⟩
+        left
+        unfold restriction
+        simp only [Set.mem_setOf_eq, mem_self_comm_mem_inv]
+        rw [← hx.right]
+        exact ⟨ht, hF.ran_ss (mem_pair_imp_snd_mem_ran ht)⟩
+
+  · intro ⟨G, hG₁, hG₂⟩
     refine ⟨hF.is_func, ?_⟩
+    unfold isSingleRooted
     intro y hy
     have ⟨x₁, hx₁⟩ := ran_exists hy
     refine ⟨x₁, ⟨mem_pair_imp_fst_mem_dom hx₁, hx₁⟩, ?_⟩
     intro x₂ hx₂
-    
+    have hc_x₁ : (x₁, x₁) ∈ comp G F := by
-    have hG' : y ∈ dom G := by
+      rw [hG₂]
-      rw [hG.left.dom_eq]
+      simp only [Set.mem_setOf_eq, and_true]
-      exact hF.ran_ss hy
+      rw [← hF.dom_eq]
-    have ⟨z, hz⟩ := dom_exists hG'
+      exact mem_pair_imp_fst_mem_dom hx₁
-
+    have hc_x₂ : (x₂, x₂) ∈ comp G F := by
-    have := hG.right
+      rw [hG₂]
-    unfold comp at this
+      simp only [Set.mem_setOf_eq, and_true]
-    rw [Set.ext_iff] at this
+      rw [← hF.dom_eq]
-    have h₁ := (this (x₁, z)).mp ⟨y, hx₁, hz⟩
+      exact hx₂.left
-    have h₂ := (this (x₂, z)).mp ⟨y, hx₂.right, hz⟩
+    unfold comp at hc_x₁ hc_x₂
-    simp only [Set.mem_setOf_eq] at h₁ h₂
+    have ⟨t₁, ht₁⟩ := hc_x₁
-    rw [h₁.right, h₂.right]
+    have ⟨t₂, ht₂⟩ := hc_x₂
-  · sorry
+    simp only at ht₁ ht₂
+    rw [← single_valued_eq_unique hF.is_func hx₁ ht₁.left] at ht₁
+    rw [← single_valued_eq_unique hF.is_func hx₂.right ht₂.left] at ht₂
+    exact single_valued_eq_unique hG₁.is_func ht₂.right ht₁.right
 
 /-- #### Theorem 3J (b)
 
@@ -147,12 +267,18 @@ Assume that `F : A → B`, and that `A` is nonempty. There exists a function
 `H : B → A` (a "right inverse") such that `F ∘ H` is the identity function on
 `B` **iff** `F` maps `A` onto `B`.
 -/
-theorem theorem_3j_b {F : Set.HRelation α β} {A : Set α} {B : Set β}
+theorem theorem_3j_b {F : Set.HRelation α β} (hF : mapsInto F A B)
-  (hF : mapsInto F A B) (hA : Set.Nonempty A)
+  : (∃ H, mapsInto H B A ∧ comp F H = { p | p.1 ∈ B ∧ p.1 = p.2 }) →
-  : (∃ H : Set.HRelation β α,
+      mapsOnto F A B := by
-      mapsInto H B A ∧
+  intro ⟨H, _, hH₂⟩
-        (comp F H = { p | p.1 ∈ B ∧ p.1 = p.2 })) ↔ mapsOnto F A B := by
+  refine ⟨hF.is_func, hF.dom_eq, Set.Subset.antisymm hF.ran_ss ?_⟩
-  sorry
+  show ∀ y, y ∈ B → y ∈ ran F
+  intro y hy
+  suffices y ∈ ran (comp F H) from ran_comp_imp_ran_self this
+  rw [hH₂]
+  unfold ran Prod.snd Set.image
+  simp only [Set.mem_setOf_eq, Prod.exists, exists_eq_right, Set.setOf_mem_eq]
+  exact hy
 
 /-- #### Theorem 3K (a)
 
@@ -331,6 +457,26 @@ theorem corollary_3l_iii {G : Set.HRelation β α} {A B : Set α}
     single_valued_self_iff_single_rooted_inv.mp hG
   exact (theorem_3k_c_ii hG').symm
 
+/-- #### Theorem 3M
+
+If `R` is a symmetric and transitive relation, then `R` is an equivalence
+relation on `fld R`.
+-/
+theorem theorem_3m {R : Set.Relation α}
+  (hS : R.isSymmetric) (hT : R.isTransitive)
+  : R.isEquivalence (fld R) := by
+  refine ⟨Eq.subset rfl, ?_, hS, hT⟩
+  intro x hx
+  apply Or.elim hx
+  · intro h
+    have ⟨y, hy⟩ := dom_exists h
+    have := hS hy
+    exact hT hy this
+  · intro h
+    have ⟨t, ht⟩ := ran_exists h
+    have := hS ht
+    exact hT this ht
+
 /-- #### Theorem 3R
 
 Let `R` be a linear ordering on `A`.
@@ -1710,25 +1856,140 @@ theorem exercise_3_29 {f : Set.HRelation α β} {G : Set.HRelation β (Set α)}
   rw [heq] at this
   exact single_valued_eq_unique hf.is_func this.right ht
 
-/-- #### Theorem 3M
+/-! #### Exercise 3.30
 
-If `R` is a symmetric and transitive relation, then `R` is an equivalence
+Assume that `F : 𝒫 A → 𝒫 A` and that `F` has the monotonicity property:
-relation on `fld R`.
+```
+X ⊆ Y ⊆ A → F(X) ⊆ F(Y).
+```
+Define `B = ⋂ {X ⊆ A | F(X) ⊆ X}` and `C = ⋃ {X ⊆ A | X ⊆ F(X)}`.
 -/
-theorem theorem_3m {R : Set.Relation α}
+
-  (hS : R.isSymmetric) (hT : R.isTransitive)
+section Exercise_3_30
-  : R.isEquivalence (fld R) := by
+
-  refine ⟨Eq.subset rfl, ?_, hS, hT⟩
+variable {F : Set α → Set α} {A B C : Set α}
+         (hF : Set.MapsTo F (𝒫 A) (𝒫 A))
+         (hMono : ∀ X Y, X ⊆ Y ∧ Y ⊆ A → F X ⊆ F Y)
+         (hB : B = ⋂₀ { X | X ⊆ A ∧ F X ⊆ X })
+         (hC : C = ⋃₀ { X | X ⊆ A ∧ X ⊆ F X })
+
+/-- ##### Exercise 3.30 (a)
+
+Show that `F(B) = B` and `F(C) = C`.
+-/
+theorem exercise_3_30_a : F B = B ∧ F C = C := by
+
+  have hB_subset : F B ⊆ B := by
     intro x hx
-  apply Or.elim hx
+    have : ∀ X, X ⊆ A ∧ F X ⊆ X → x ∈ X := by
-  · intro h
+      intro X ⟨hX₁, hX₂⟩
-    have ⟨y, hy⟩ := dom_exists h
+      have hB₁ : B ⊆ X := by
-    have := hS hy
+        show ∀ t, t ∈ B → t ∈ X
-    exact hT hy this
+        intro t ht
-  · intro h
+        rw [hB] at ht
-    have ⟨t, ht⟩ := ran_exists h
+        simp only [Set.mem_sInter] at ht 
-    have := hS ht
+        exact ht X ⟨hX₁, hX₂⟩
-    exact hT this ht
+      exact hX₂ (hMono B X ⟨hB₁, hX₁⟩ hx)
+    rw [hB]
+    exact this
+  
+  have hC_supset : C ⊆ F C := by
+    intro x hx
+    rw [hC] at hx
+    simp only [Set.mem_sUnion, Set.mem_setOf_eq] at hx
+    have ⟨X, hX⟩ := hx
+    have hC₁ : X ⊆ C := by
+      show ∀ t, t ∈ X → t ∈ C
+      intro t ht
+      rw [hC]
+      simp only [Set.mem_sUnion, Set.mem_setOf_eq]
+      exact ⟨X, hX.left, ht⟩
+    have hC₂ : C ⊆ A := by
+      show ∀ t, t ∈ C → t ∈ A
+      intro t ht
+      rw [hC] at ht
+      simp only [Set.mem_sUnion, Set.mem_setOf_eq] at ht
+      have ⟨T, hT⟩ := ht
+      exact hT.left.left hT.right
+    exact hMono X C ⟨hC₁, hC₂⟩ (hX.left.right hX.right)
+  
+  have hC_sub_A : C ⊆ A := by
+    show ∀ t, t ∈ C → t ∈ A
+    intro t ht
+    rw [hC] at ht
+    simp at ht
+    have ⟨X, hX⟩ := ht
+    exact hX.left.left hX.right
+
+  have hFC_sub_A : F C ⊆ A := by
+    show ∀ t, t ∈ F C → t ∈ A
+    intro t ht
+    have := hF hC_sub_A
+    simp only [Set.mem_powerset_iff] at this
+    exact this ht
+
+  have hC_subset : F C ⊆ C := by
+    suffices ∀ X, X ∈ {X | X ⊆ A ∧ X ⊆ F X} → X ⊆ C from
+      this (F C) ⟨hFC_sub_A, hMono C (F C) ⟨hC_supset, hFC_sub_A⟩⟩
+    intro X hX
+    simp at hX
+    rw [hC]
+    show ∀ t, t ∈ X → t ∈ ⋃₀ {X | X ⊆ A ∧ X ⊆ F X}
+    intro t ht
+    simp only [Set.mem_sUnion, Set.mem_setOf_eq]
+    exact ⟨X, hX, ht⟩
+  
+  have hB_sub_A : B ⊆ A := by
+    show ∀ t, t ∈ B → t ∈ A
+    intro t ht
+    rw [hB] at ht
+    simp only [Set.mem_sInter, Set.mem_setOf_eq] at ht
+    have := ht C ⟨hC_sub_A, hC_subset⟩
+    exact hC_sub_A this
+
+  apply And.intro
+  · rw [Set.Subset.antisymm_iff]
+    apply And.intro
+    · exact hB_subset
+    · have hInter : ∀ X, X ∈ {X | X ⊆ A ∧ F X ⊆ X} → B ⊆ X := by
+        intro X hX
+        simp only [Set.mem_setOf_eq] at hX 
+        rw [hB]
+        show ∀ t, t ∈ ⋂₀ {X | X ⊆ A ∧ F X ⊆ X} → t ∈ X
+        intro t ht
+        simp only [Set.mem_sInter, Set.mem_setOf_eq] at ht 
+        exact ht X hX
+      refine hInter (F B) ⟨?_, ?_⟩
+      · show ∀ t, t ∈ F B → t ∈ A
+        intro t ht
+        have := hF hB_sub_A
+        simp only [Set.mem_powerset_iff] at this
+        exact this ht
+      · refine hMono (F B) B ⟨hB_subset, hB_sub_A⟩
+  · rw [Set.Subset.antisymm_iff]
+    exact ⟨hC_subset, hC_supset⟩
+
+/-- ##### Exercise 3.30 (b)
+
+Show that if `F(X) = X`, then `B ⊆ X ⊆ C`.
+-/
+theorem exercise_3_30_b : ∀ X, X ⊆ A ∧ F X = X → B ⊆ X ∧ X ⊆ C := by
+  intro X ⟨hX₁, hX₂⟩
+  apply And.intro
+  · have : F X ⊆ X := Eq.subset hX₂
+    rw [hB]
+    show ∀ t, t ∈ ⋂₀ {X | X ⊆ A ∧ F X ⊆ X} → t ∈ X
+    intro t ht
+    simp only [Set.mem_sInter, Set.mem_setOf_eq] at ht 
+    exact ht X ⟨hX₁, this⟩
+  · have : X ⊆ F X := Eq.subset (id (Eq.symm hX₂))
+    rw [hC]
+    show ∀ t, t ∈ X → t ∈ ⋃₀ {X | X ⊆ A ∧ X ⊆ F X}
+    intro t ht
+    simp only [Set.mem_sUnion, Set.mem_setOf_eq]
+    exact ⟨X, ⟨hX₁, this⟩, ht⟩
+
+end Exercise_3_30
 
 /-- #### Exercise 3.32 (a)