Enderton. Add additional definitions and prove Theorem 3E.

Bookshelf/Enderton/Set.tex

@@ -24,12 +24,18 @@
 \chapter{Reference}%
 \label{chap:reference}
 
-\section{\partial{Composition}}%
+\section{\defined{Composition}}%
 \label{ref:composition}
 
 The \textbf{composition} of sets $F$ and $G$ is
   $$F \circ G = \{\left< u, v \right> \mid \exists t(uGt \land tFv)\}.$$
 
+\begin{definition}
+
+  \lean*{Common/Set/Relation}{Set.Relation.comp}
+
+\end{definition}
+
 \section{\defined{Domain}}%
 \label{ref:domain}
 
@@ -105,7 +111,7 @@ One-to-one functions are sometimes called \textbf{injections}.
 
 \end{definition}
 
-\section{\partial{Image}}%
+\section{\defined{Image}}%
 \label{ref:image}
 
 Let $A$ and $F$ be arbitrary sets.
@@ -116,12 +122,24 @@ The \textbf{image of $A$ under $F$} is the set
       & = \{v \mid (\exists u \in A) uFv\}.
   \end{align*}
 
-\section{\partial{Inverse}}%
+\begin{definition}
+
+  \lean*{Common/Set/Relation}{Set.Relation.image}
+
+\end{definition}
+
+\section{\defined{Inverse}}%
 \label{ref:inverse}
 
 The \textbf{inverse} of a set $F$ is the set
   $$F^{-1} = \{\left< u, v \right> \mid vFu\}.$$
 
+\begin{definition}
+
+  \lean*{Common/Set/Relation}{Set.Relation.inv}
+
+\end{definition}
+
 \section{\defined{Ordered Pair}}%
 \label{ref:ordered-pair}
 
@@ -214,12 +232,18 @@ A \textbf{relation} is a set of \nameref{ref:ordered-pair}s.
 
 \end{definition}
 
-\section{\partial{Restriction}}%
+\section{\defined{Restriction}}%
 \label{ref:restriction}
 
 The \textbf{restriction} of a set $F$ to set $A$ is the set
   $$F \restriction A = \{\left< u, v \right> \mid uFv \land u \in A\}.$$
 
+\begin{definition}
+
+  \lean*{Common/Set/Relation}{Set.Relation.restriction}
+
+\end{definition}
+
 \section{\defined{Subset Axioms}}%
 \label{ref:subset-axioms}
 
@@ -2997,7 +3021,7 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive
 \section{Functions}%
 \label{sec:functions}
 
-\subsection{\partial{Theorem 3E}}%
+\subsection{\verified{Theorem 3E}}%
 \label{sub:theorem-3e}
 
 \begin{theorem}[3E]
@@ -3009,6 +3033,17 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive
 
 \begin{proof}
 
+  \statementpadding
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3e\_i}
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3e\_ii}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3e\_iii}
+
   We prove that (i) $\dom{(F^{-1})} = \ran{F}$, (ii) $\ran{(F^{-1})} = \dom{F}$,
     and (iii) $(F^{-1})^{-1} = F$.
 
@@ -3056,6 +3091,14 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive
 
 \begin{proof}
 
+  \statementpadding
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3f\_i}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3f\_ii}
+
   TODO
 
 \end{proof}

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -100,20 +100,20 @@ theorem exercise_5_3 {A : Set (Set α)} {𝓑 : Set (Set β)}
       ext x
       rw [Set.mem_setOf_eq]
       apply Iff.intro
-      · intro ⟨h₁, ⟨b, h₂⟩⟩
+      · intro ⟨h₁, b, h₂⟩
-        exact ⟨b, ⟨h₂.left, ⟨h₁, h₂.right⟩⟩⟩
+        exact ⟨b, h₂.left, h₁, h₂.right⟩
-      · intro ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩
+      · intro ⟨b, h₁, h₂, h₃⟩
-        exact ⟨h₂, ⟨b, ⟨h₁, h₃⟩⟩⟩
+        exact ⟨h₂, b, h₁, h₃⟩
     _ = ⋃₀ { Set.prod A p | p ∈ 𝓑 } := by
       ext x
       rw [Set.mem_setOf_eq]
       unfold Set.sUnion sSup Set.instSupSetSet
       simp only [Set.mem_setOf_eq, exists_exists_and_eq_and]
       apply Iff.intro
-      · intro ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩
+      · intro ⟨b, h₁, h₂, h₃⟩
-        exact ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩
+        exact ⟨b, h₁, h₂, h₃⟩
-      · intro ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩
+      · intro ⟨b, h₁, h₂, h₃⟩
-        exact ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩
+        exact ⟨b, h₁, h₂, h₃⟩
 
 /-- ### Exercise 5.5a
 
@@ -268,7 +268,7 @@ theorem exercise_6_7 {R : Set.Relation α}
         Set.mem_image, Prod.exists, exists_and_right, exists_eq_right
       ] at hd
       have ⟨y, hp⟩ := hd
-      have hm : OrderedPair x y ∈ R.image (fun p => OrderedPair p.1 p.2) := by
+      have hm : OrderedPair x y ∈ Set.image (fun p => OrderedPair p.1 p.2) R := by
         unfold Set.image
         simp only [Prod.exists, Set.mem_setOf_eq]
         exact ⟨x, ⟨y, ⟨hp, rfl⟩⟩⟩
@@ -279,7 +279,7 @@ theorem exercise_6_7 {R : Set.Relation α}
       unfold Set.Relation.ran Prod.snd at hr
       simp only [Set.mem_image, Prod.exists, exists_eq_right] at hr
       have ⟨t, ht⟩ := hr
-      have hm : OrderedPair t x ∈ R.image (fun p => OrderedPair p.1 p.2) := by
+      have hm : OrderedPair t x ∈ Set.image (fun p => OrderedPair p.1 p.2) R := by
         simp only [Set.mem_image, Prod.exists]
         exact ⟨t, ⟨x, ⟨ht, rfl⟩⟩⟩
       unfold OrderedPair at hm
@@ -329,7 +329,7 @@ theorem exercise_6_7 {R : Set.Relation α}
       simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at this
       exact hxy_mem this
 
-/-- ### Exercise 6.8i
+/-- ### Exercise 6.8 (i)
 
 Show that for any set `𝓐`:
 ```
@@ -350,12 +350,12 @@ theorem exercise_6_8_i {A : Set (Set.Relation α)}
     exists_exists_and_eq_and
   ]
   apply Iff.intro
-  · intro ⟨y, ⟨t, ⟨ht, hx⟩⟩⟩
+  · intro ⟨y, t, ht, hx⟩
-    exact ⟨t, ⟨ht, ⟨y, hx⟩⟩⟩
+    exact ⟨t, ht, y, hx⟩
-  · intro ⟨t, ⟨ht, ⟨y, hx⟩⟩⟩
+  · intro ⟨t, ht, y, hx⟩
-    exact ⟨y, ⟨t, ⟨ht, hx⟩⟩⟩
+    exact ⟨y, t, ht, hx⟩
 
-/-- ### Exercise 6.8ii
+/-- ### Exercise 6.8 (ii)
 
 Show that for any set `𝓐`:
 ```
@@ -380,7 +380,7 @@ theorem exercise_6_8_ii {A : Set (Set.Relation α)}
   · intro ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩
     exact ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩
 
-/-- ## Exercise 6.9i
+/-- ### Exercise 6.9 (i)
 
 Discuss the result of replacing the union operation by the intersection
 operation in the preceding problem.
@@ -406,7 +406,7 @@ theorem exercise_6_9_i {A : Set (Set.Relation α)}
   intro _ y hy R hR
   exact ⟨y, hy R hR⟩
 
-/-- ## Exercise 6.9ii
+/-- ### Exercise 6.9 (ii)
 
 Discuss the result of replacing the union operation by the intersection
 operation in the preceding problem.
@@ -432,4 +432,86 @@ theorem exercise_6_9_ii {A : Set (Set.Relation α)}
   intro _ y hy R hR
   exact ⟨y, hy R hR⟩
 
+/-- ### Theorem 3E (i)
+
+For a set `F`, `dom F⁻¹ = ran F`.
+-/
+theorem theorem_3e_i {F : Set.Relation α}
+  : Set.Relation.dom (F.inv) = Set.Relation.ran F := by
+  ext x
+  unfold Set.Relation.dom Set.Relation.ran Set.Relation.inv
+  simp only [
+    Prod.exists,
+    Set.mem_image,
+    Set.mem_setOf_eq,
+    Prod.mk.injEq,
+    exists_and_right,
+    exists_eq_right
+  ]
+  apply Iff.intro
+  · intro ⟨y, a, _, h⟩
+    rw [← h.right.left]
+    exact ⟨a, h.left⟩
+  · intro ⟨y, hy⟩
+    exact ⟨y, y, x, hy, rfl, rfl⟩
+
+/-- ### Theorem 3E (ii)
+
+For a set `F`, `ran F⁻¹ = dom F`.
+-/
+theorem theorem_3e_ii {F : Set.Relation α}
+  : Set.Relation.ran (F.inv) = Set.Relation.dom F := by
+  ext x
+  unfold Set.Relation.dom Set.Relation.ran Set.Relation.inv
+  simp only [
+    Prod.exists,
+    Set.mem_image,
+    Set.mem_setOf_eq,
+    Prod.mk.injEq,
+    exists_eq_right,
+    exists_and_right
+  ]
+  apply Iff.intro
+  · intro ⟨a, y, b, h⟩
+    rw [← h.right.right]
+    exact ⟨b, h.left⟩
+  · intro ⟨y, hy⟩
+    exact ⟨y, x, y, hy, rfl, rfl⟩
+
+/-- ### Theorem 3E (iii)
+
+For a set `F`, `(F⁻¹)⁻¹ = F`.
+-/
+theorem theorem_3e_iii {F : Set.Relation α}
+  : F.inv.inv = F := by
+  unfold Set.Relation.inv
+  simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq]
+  ext x
+  apply Iff.intro
+  · intro hx
+    have ⟨a₁, b₁, ⟨⟨a₂, b₂, h₁⟩, h₂⟩⟩ := hx
+    rw [← h₂, ← h₁.right.right, ← h₁.right.left]
+    exact h₁.left
+  · intro hx
+    have (p, q) := x
+    refine ⟨q, p, ⟨?_, ?_⟩⟩
+    · exact ⟨p, q, hx, rfl, rfl⟩
+    · rfl
+
+/-- ### Theorem 3F (i)
+
+For a set `F`, `F⁻¹` is a function **iff** `F` is single-rooted.
+-/
+theorem theorem_3f_i {F : Set.Relation α}
+  : Set.Relation.isSingleValued F.inv ↔ Set.Relation.isSingleRooted F := by
+  sorry
+
+/-- ### Theorem 3F (ii)
+
+For a relation `F`, `F` is a function **iff** `F⁻¹` is single-rooted.
+-/
+theorem theorem_3f_ii {F : Set.Relation α}
+  : Set.Relation.isSingleValued F ↔ Set.Relation.isSingleRooted F.inv := by
+  sorry
+
 end Enderton.Set.Chapter_3

Common/Set/Relation.lean

@@ -37,11 +37,51 @@ The field of a `Relation`.
 -/
 def fld (R : Relation α) : Set α := dom R ∪ ran R
 
+/--
+The inverse of a `Relation`.
+-/
+def inv (R : Relation α) : Relation α := { (p.2, p.1) | p ∈ R }
+
+/--
+The composition of two `Relation`s.
+-/
+def comp (F G : Relation α) : Relation α :=
+  { p | ∃ t, (p.1, t) ∈ G ∧ (t, p.2) ∈ F}
+
+/--
+The restriction of a `Relation` to a `Set`.
+-/
+def restriction (R : Relation α) (A : Set α) : Relation α :=
+  { p ∈ R | p.1 ∈ A } 
+
+/--
+The image of a `Relation` under a `Set`.
+-/
+def image (R : Relation α) (A : Set α) : Set α :=
+  { y | ∃ u ∈ A, (u, y) ∈ R }
+
+/--
+A `Relation` `R` is said to be single-rooted **iff** for all `y ∈ ran R`, there
+exists exactly one `x` such that `⟨x, y⟩ ∈ R`.
+-/
+def isSingleRooted (R : Relation α) : Prop :=
+  ∀ y ∈ R.ran, ∃! x, x ∈ R.dom ∧ (x, y) ∈ R
+
+/--
+A `Relation` `R` is said to be single-valued **iff** for all `x ∈ dom R`, there
+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
+
 /--
 Convert a `Relation` into an equivalent representation using `OrderedPair`s.
 -/
 def toOrderedPairs (R : Relation α) : Set (Set (Set α)) :=
-  R.image (fun (x, y) => OrderedPair x y)
+  -- Notice here we are using `Set.image` and *not* `Set.Relation.image`.
+  Set.image (fun (x, y) => OrderedPair x y) R
 
 end Relation