Enderton. Formally verify exercises 3.12 through 3.15.

Bookshelf/Enderton/Set.tex

@@ -3949,7 +3949,7 @@ Then $F = G$.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.12}}%
+\subsection{\verified{Exercise 3.12}}%
 \label{sub:exercise-3.12}
 
 Assume that $f$ and $g$ are functions and show that
@@ -3958,6 +3958,9 @@ Assume that $f$ and $g$ are functions and show that
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_12}
+
   Let $f$ and $g$ be \nameref{ref:function}s.
 
   \paragraph{($\Rightarrow$)}%
@@ -3982,7 +3985,7 @@ Assume that $f$ and $g$ are functions and show that
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.13}}%
+\subsection{\verified{Exercise 3.13}}%
 \label{sub:exercise-3.13}
 
 Assume that $f$ and $g$ are functions with $f \subseteq g$ and
@@ -3991,6 +3994,9 @@ Show that $f = g$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_13}
+
   Let $f$ and $g$ be functions such that $f \subseteq g$ and
     $\dom{g} \subseteq \dom{f}$.
   By \nameref{sub:exercise-3.12}, it follows that $\dom{f} \subseteq \dom{g}$
@@ -4001,7 +4007,7 @@ Show that $f = g$.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.14}}%
+\subsection{\verified{Exercise 3.14}}%
 \label{sub:exercise-3.14}
 
 Assume that $f$ and $g$ are functions.
@@ -4014,17 +4020,22 @@ Assume that $f$ and $g$ are functions.
 
 \begin{proof}
 
-  Assume $f$ and $g$ are functions.
+  \statementpadding
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_14\_a}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_14\_b}
+
+  Assume $f$ and $g$ are \nameref{ref:function}s.
 
   \paragraph{(a)}%
 
     Consider $f \cap g$.
     By definition of the intersection of sets, $f \cap g \subseteq f$.
-    By \nameref{sub:exercise-3.12}, $\dom{(f \cap g)} = \dom{f}$ and
+    Since $f$ is single-valued, it trivially follows that so must $f \cap g$.
-      $(\forall x \in \dom{(f \cap g)} (f \cap g)(x) = f(x)$.
+    Therefore $f \cap g$ is a function.
-    The latter conjunct shows that, since $f$ is single-valued, $f \cap g$ must
-      also be single-valued.
-    In other words, $f \cap g$ is a function.
 
   \paragraph{(b)}%
 
@@ -4064,7 +4075,7 @@ Assume that $f$ and $g$ are functions.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.15}}%
+\subsection{\verified{Exercise 3.15}}%
 \label{sub:exercise-3.15}
 
 Let $\mathscr{A}$ be a set of functions such that for any $f$ and $g$ in
@@ -4073,6 +4084,9 @@ Show that $\bigcup{\mathscr{A}}$ is a function.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_3\_15}
+
   Let $\mathscr{A}$ be a set of \nameref{ref:function}s such that for any $f$
     and $g$ in $\mathscr{A}$, either $f \subseteq g$ or $g \subseteq f$.
   Let $x \in \dom{\bigcup{\mathscr{A}}}$.

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -325,7 +325,7 @@ theorem exercise_3_7 {R : Set.Relation α}
       simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at this
       exact hxy_mem this
 
-section
+section Relation
 
 open Set.Relation
 
@@ -678,11 +678,8 @@ theorem theorem_3k_c_ii {F : Set.Relation α} {A B : Set α}
     unfold image at nv
     simp only [Set.mem_setOf_eq] at nv
     have ⟨u₁, hu₁⟩ := nv
-    have ⟨x, hx⟩ := hF v (mem_pair_imp_snd_mem_ran hu.right)
+    have := single_rooted_eq_unique hF hu.right hu₁.right
-    simp only [and_imp] at hx
+    rw [← this] at hu₁
-    have hr₁ := hx.right u (mem_pair_imp_fst_mem_dom hu.right) hu.right
-    have hr₂ := hx.right u₁ (mem_pair_imp_fst_mem_dom hu₁.right) hu₁.right
-    rw [hr₂, ← hr₁] at hu₁
     exact absurd hu₁.left hu.left.right
   exact ⟨hv₁, hv₂⟩
 
@@ -714,6 +711,173 @@ theorem corollary_3l_iii {G : Set.Relation α} {A B : Set α}
     single_valued_self_iff_single_rooted_inv.mp hG
   exact (theorem_3k_c_ii hG').symm
 
-end
+/-- #### Exercise 3.12
+
+Assume that `f` and `g` are functions and show that
+```
+f ⊆ g ↔ dom f ⊆ dom g ∧ (∀ x ∈ dom f) f(x) = g(x).
+```
+-/
+theorem exercise_3_12 {f g : Set.Relation α}
+  (hf : f.isSingleValued) (_ : g.isSingleValued)
+  : f ⊆ g ↔ dom f ⊆ dom g ∧ (∀ x ∈ dom f, ∃! y : α, (x, y) ∈ f ∧ (x, y) ∈ g) := by
+  apply Iff.intro
+  · intro h
+    apply And.intro
+    · show ∀ x, x ∈ dom f → x ∈ dom g
+      intro x hx
+      have ⟨y, hy⟩ := dom_exists hx
+      exact mem_pair_imp_fst_mem_dom (h hy)
+    · intro x hx
+      have ⟨y, hy⟩ := dom_exists hx
+      refine ⟨y, ⟨hy, h hy⟩, ?_⟩
+      intro y₁ hy₁
+      exact single_valued_eq_unique hf hy₁.left hy
+  · intro ⟨_, hx⟩
+    show ∀ p, p ∈ f → p ∈ g
+    intro (x, y) hp
+    have ⟨y₁, hy₁⟩ := hx x (mem_pair_imp_fst_mem_dom hp)
+    rw [single_valued_eq_unique hf hp hy₁.left.left]
+    exact hy₁.left.right
+
+/-- #### Exercise 3.13
+
+Assume that `f` and `g` are functions with `f ⊆ g` and `dom g ⊆ dom f`. Show
+that `f = g`.
+-/
+theorem exercise_3_13 {f g : Set.Relation α}
+  (hf : f.isSingleValued) (hg : g.isSingleValued)
+  (h : f ⊆ g) (h₁ : dom g ⊆ dom f)
+  : f = g := by
+  have h₂ := (exercise_3_12 hf hg).mp h
+  have hfg := Set.Subset.antisymm_iff.mpr ⟨h₁, h₂.left⟩
+  ext p
+  have (a, b) := p
+  apply Iff.intro
+  · intro hp
+    have ⟨x, hx⟩ := h₂.right a (mem_pair_imp_fst_mem_dom hp)
+    rw [single_valued_eq_unique hf hp hx.left.left]
+    exact hx.left.right
+  · intro hp
+    rw [← hfg] at h₂
+    have ⟨x, hx⟩ := h₂.right a (mem_pair_imp_fst_mem_dom hp)
+    rw [single_valued_eq_unique hg hp hx.left.right]
+    exact hx.left.left
+
+/-- #### Exercise 3.14 (a)
+
+Assume that `f` and `g` are functions. Show that `f ∩ g` is a function.
+-/
+theorem exercise_3_14_a {f g : Set.Relation α}
+  (hf : f.isSingleValued) (_ : g.isSingleValued)
+  : (f ∩ g).isSingleValued :=
+  single_valued_subset hf (Set.inter_subset_left f g)
+
+/-- #### Exercise 3.14 (b)
+
+Assume that `f` and `g` are functions. Show that `f ∪ g` is a function **iff**
+`f(x) = g(x)` for every `x` in `(dom f) ∩ (dom g)`.
+-/
+theorem exercise_3_14_b {f g : Set.Relation α}
+  (hf : f.isSingleValued) (hg : g.isSingleValued)
+  : (f ∪ g).isSingleValued ↔
+      (∀ x ∈ dom f ∩ dom g, ∃! y, (x, y) ∈ f ∧ (x, y) ∈ g) := by
+  apply Iff.intro
+  · intro h x hx
+    have ⟨y₁, hy₁⟩ := hf x hx.left
+    have ⟨y₂, hy₂⟩ := hg x hx.right
+    have : y₁ = y₂ := by
+      have hf' : (x, y₁) ∈ f ∪ g := Or.inl hy₁.left.right
+      have hg' : (x, y₂) ∈ f ∪ g := Or.inr hy₂.left.right
+      exact single_valued_eq_unique h hf' hg'
+    rw [← this] at hy₂
+    refine ⟨y₁, ⟨hy₁.left.right, hy₂.left.right⟩, ?_⟩
+    intro y₃ hfy₃
+    exact single_valued_eq_unique hf hfy₃.left hy₁.left.right
+  · intro h x hx
+    by_cases hfx : x ∈ dom f
+    · by_cases hgx : x ∈ dom g
+      · -- `x ∈ dom f ∧ x ∈ dom g`
+        have ⟨y₁, hy₁⟩ := hf x hfx
+        have ⟨y₂, hy₂⟩ := hg x hgx
+        refine ⟨y₁, ⟨?_, Or.inl hy₁.left.right⟩, ?_⟩
+        · unfold ran
+          simp only [Set.mem_image, Set.mem_union, Prod.exists, exists_eq_right]
+          exact ⟨x, Or.inl hy₁.left.right⟩
+        · intro y₃ hy₃
+          apply Or.elim hy₃.right
+          · intro hxy
+            exact single_valued_eq_unique hf hxy hy₁.left.right
+          · refine fun hxy => single_valued_eq_unique hg hxy ?_
+            have : y₁ = y₂ := by
+              have ⟨z, ⟨hz, _⟩⟩ := h x ⟨hfx, hgx⟩
+              rw [
+                single_valued_eq_unique hf hy₁.left.right hz.left,
+                single_valued_eq_unique hg hy₂.left.right hz.right
+              ]
+            rw [this]
+            exact hy₂.left.right
+      · -- `x ∈ dom f ∧ x ∉ dom g`
+        have ⟨y, hy⟩ := dom_exists hfx
+        have hxy : (x, y) ∈ f ∪ g := (Set.subset_union_left f g) hy
+        refine ⟨y, ⟨mem_pair_imp_snd_mem_ran hxy, hxy⟩, ?_⟩
+        intro y₁ hy₁
+        apply Or.elim hy₁.right
+        · intro hx'
+          exact single_valued_eq_unique hf hx' hy
+        · intro hx'
+          exact absurd (mem_pair_imp_fst_mem_dom hx') hgx
+    · by_cases hgx : x ∈ dom g
+      · -- `x ∉ dom f ∧ x ∈ dom g`
+        have ⟨y, hy⟩ := dom_exists hgx
+        have hxy : (x, y) ∈ f ∪ g := (Set.subset_union_right f g) hy
+        refine ⟨y, ⟨mem_pair_imp_snd_mem_ran hxy, hxy⟩, ?_⟩
+        intro y₁ hy₁
+        apply Or.elim hy₁.right
+        · intro hx'
+          exact absurd (mem_pair_imp_fst_mem_dom hx') hfx
+        · intro hx'
+          exact single_valued_eq_unique hg hx' hy
+      · -- `x ∉ dom f ∧ x ∉ dom g`
+        exfalso
+        unfold dom at hx
+        simp only [
+          Set.mem_image,
+          Set.mem_union,
+          Prod.exists,
+          exists_and_right,
+          exists_eq_right
+        ] at hx
+        have ⟨_, hy⟩ := hx
+        apply Or.elim hy
+        · intro hz
+          exact absurd (mem_pair_imp_fst_mem_dom hz) hfx
+        · intro hz
+          exact absurd (mem_pair_imp_fst_mem_dom hz) hgx
+
+/-- #### Exercise 3.15
+
+Let `𝓐` be a set of functions such that for any `f` and `g` in `𝓐`, either
+`f ⊆ g` or `g ⊆ f`. Show that `⋃ 𝓐` is a function.
+-/
+theorem exercise_3_15 {𝓐 : Set (Set.Relation α)}
+  (h𝓐 : ∀ F ∈ 𝓐, F.isSingleValued)
+  (h : ∀ F, ∀ G, F ∈ 𝓐 → G ∈ 𝓐 → F ⊆ G ∨ G ⊆ F)
+  : isSingleValued (⋃₀ 𝓐) := by
+  intro x hx
+  have ⟨y₁, hy₁⟩ := dom_exists hx
+  refine ⟨y₁, ⟨mem_pair_imp_snd_mem_ran hy₁, hy₁⟩, ?_⟩
+  intro y₂ hy₂
+  have ⟨f, hf⟩ : ∃ f : Set.Relation α, f ∈ 𝓐 ∧ (x, y₁) ∈ f := hy₁
+  have ⟨g, hg⟩ : ∃ g : Set.Relation α, g ∈ 𝓐 ∧ (x, y₂) ∈ g := hy₂.right
+  apply Or.elim (h f g hf.left hg.left)
+  · intro hf'
+    have := hf' hf.right
+    exact single_valued_eq_unique (h𝓐 g hg.left) hg.right this
+  · intro hg'
+    have := hg' hg.right
+    exact single_valued_eq_unique (h𝓐 f hf.left) this hf.right
+
+end Relation
 
 end Enderton.Set.Chapter_3

Bookshelf/Enderton/Set/Relation.lean

@@ -180,7 +180,7 @@ A `Relation` `R` is said to be single-rooted **iff** for all `y ∈ ran R`, ther
 exists exactly one `x` such that `⟨x, y⟩ ∈ R`.
 -/
 def isSingleRooted (R : Relation α) : Prop :=
-  ∀ y ∈ R.ran, ∃! x, x ∈ R.dom ∧ (x, y) ∈ R
+  ∀ y ∈ ran R, ∃! x, x ∈ dom R ∧ (x, y) ∈ R
 
 /--
 A single-rooted `Relation` should map the same output to the same input.
@@ -204,7 +204,7 @@ exists exactly one `y` such that `⟨x, y⟩ ∈ R`.
 Notice, a `Relation` that is single-valued is a function.
 -/
 def isSingleValued (R : Relation α) : Prop :=
-  ∀ x ∈ R.dom, ∃! y, y ∈ R.ran ∧ (x, y) ∈ R
+  ∀ x ∈ dom R, ∃! y, y ∈ ran R ∧ (x, y) ∈ R
 
 /--
 A single-valued `Relation` should map the same input to the same output.
@@ -263,6 +263,21 @@ theorem single_valued_self_iff_single_rooted_inv {F : Set.Relation α}
   conv => lhs; rw [← inv_inv_eq_self F]
   rw [single_valued_inv_iff_single_rooted_self]
 
+/--
+The subset of a function must also be a function.
+-/
+theorem single_valued_subset {F G : Set.Relation α}
+  (hG : G.isSingleValued) (h : F ⊆ G)
+  : F.isSingleValued := by
+  unfold isSingleValued
+  intro x hx
+  have ⟨y, hy⟩ := dom_exists hx
+  unfold ExistsUnique
+  simp only
+  refine ⟨y, ⟨mem_pair_imp_snd_mem_ran hy, hy⟩, ?_⟩
+  intro y₁ hy₁
+  exact single_valued_eq_unique hG (h hy₁.right) (h hy)
+
 /--
 A `Relation` `R` is one-to-one if it is a single-rooted function.
 -/