Enderton. Break out relations/ordered pairs. Exercise 6.7.

Bookshelf/Enderton/Set.tex

@@ -2744,13 +2744,16 @@ Show that a set $A$ is a relation iff $A \subseteq \dom{A} \times \ran{A}$.
 
 \end{proof}
 
-\subsection{\partial{Exercise 6.7}}%
+\subsection{\verified{Exercise 6.7}}%
 \label{sub:exercise-6.7}
 
 Show that if $R$ is a relation, then $\fld{R} = \bigcup\bigcup R$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_6\_7}
+
   Let $R$ be a \nameref{ref:relation}.
   We show that (i) $\fld{R} \subseteq \bigcup\bigcup R$ and (ii) that
     $\bigcup\bigcup R \subseteq \fld{R}$.

Bookshelf/Enderton/Set/Chapter_2.lean

@@ -80,7 +80,7 @@ Show that every member of a set `A` is a subset of `U A`. (This was stated as an
 example in this section.)
 -/
 theorem exercise_3_3 {A : Set (Set α)}
-  : ∀ x ∈ A, x ⊆ Set.sUnion A := by
+  : ∀ x ∈ A, x ⊆ ⋃₀ A := by
   intro x hx
   show ∀ y ∈ x, y ∈ { a | ∃ t, t ∈ A ∧ a ∈ t }
   intro y hy

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -1,8 +1,6 @@
-import Mathlib.Data.Set.Basic
-
 import Bookshelf.Enderton.Set.Chapter_2
-import Common.Logic.Basic
-import Common.Set.Basic
+import Common.Set.OrderedPair
+import Common.Set.Relation
 
 /-! # Enderton.Chapter_3
 
@@ -11,107 +9,14 @@ Relations and Functions
 
 namespace Enderton.Set.Chapter_3
 
-/-! ## Ordered Pairs -/
-
-/--
-Kazimierz Kuratowski's definition of an ordered pair.
--/
-def OrderedPair (x : α) (y : β) : Set (Set (α ⊕ β)) :=
-  {{Sum.inl x}, {Sum.inl x, Sum.inr y}}
-
-namespace OrderedPair
-
-/--
-For any sets `x`, `y`, `u`, and `v`, `⟨u, v⟩ = ⟨x, y⟩` **iff** `u = x ∧ v = y`.
--/
-theorem ext_iff {x u : α} {y v : β}
-  : (OrderedPair x y = OrderedPair u v) ↔ (x = u ∧ y = v) := by
-  unfold OrderedPair
-  apply Iff.intro
-  · intro h
-    have hu := Set.ext_iff.mp h {Sum.inl u}
-    have huv := Set.ext_iff.mp h {Sum.inl u, Sum.inr v}
-    simp only [
-      Set.mem_singleton_iff,
-      Set.mem_insert_iff,
-      true_or,
-      iff_true
-    ] at hu
-    simp only [
-      Set.mem_singleton_iff,
-      Set.mem_insert_iff,
-      or_true,
-      iff_true
-    ] at huv
-    apply Or.elim hu
-    · apply Or.elim huv
-      · -- #### Case 1
-        -- `{u} = {x}` and `{u, v} = {x}`.
-        intro huv_x hu_x
-        rw [Set.singleton_eq_singleton_iff] at hu_x
-        rw [hu_x] at huv_x
-        have hx_v := Set.pair_eq_singleton_mem_imp_eq_self huv_x
-        rw [hu_x, hx_v] at h
-        simp only [Set.mem_singleton_iff, Set.insert_eq_of_mem] at h
-        have := Set.pair_eq_singleton_mem_imp_eq_self $
-          Set.pair_eq_singleton_mem_imp_eq_self h
-        rw [← hx_v] at this
-        injection hu_x with p
-        injection this with q
-        exact ⟨p.symm, q⟩
-      · -- #### Case 2
-        -- `{u} = {x}` and `{u, v} = {x, y}`.
-        intro huv_xy hu_x
-        rw [Set.singleton_eq_singleton_iff] at hu_x
-        rw [hu_x] at huv_xy
-        by_cases hx_v : Sum.inl x = Sum.inr v
-        · rw [hx_v] at huv_xy
-          simp at huv_xy
-          have := Set.pair_eq_singleton_mem_imp_eq_self huv_xy.symm
-          injection hu_x with p
-          injection this with q
-          exact ⟨p.symm, q⟩
-        · rw [Set.ext_iff] at huv_xy
-          have := huv_xy (Sum.inr v)
-          simp at this
-          injection hu_x with p
-          exact ⟨p.symm, this.symm⟩
-    · apply Or.elim huv
-      · -- #### Case 3
-        -- `{u} = {x, y}` and `{u, v} = {x}`.
-        intro huv_x _
-        rw [Set.ext_iff] at huv_x
-        have hv_x := huv_x (Sum.inr v)
-        simp only [
-          Set.mem_singleton_iff,
-          Set.mem_insert_iff,
-          or_true,
-          true_iff
-        ] at hv_x
-      · -- #### Case 4
-        -- `{u} = {x, y}` and `{u, v} = {x, y}`.
-        intro _ hu_xy
-        rw [Set.ext_iff] at hu_xy
-        have hy_u := hu_xy (Sum.inr y)
-        simp only [
-          Set.mem_singleton_iff,
-          Set.mem_insert_iff,
-          or_true,
-          iff_true
-        ] at hy_u
-  · intro h
-    rw [h.left, h.right]
-
-end OrderedPair
-
 /-- ### Theorem 3B
 
 If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`.
 -/
-theorem theorem_3b {C : Set (α ⊕ α)} (hx : Sum.inl x ∈ C) (hy : Sum.inr y ∈ C)
+theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
   : OrderedPair x y ∈ 𝒫 𝒫 C := by
-  have hxs : {Sum.inl x} ⊆ C := Set.singleton_subset_iff.mpr hx
-  have hxys : {Sum.inl x, Sum.inr y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
+  have hxs : {x} ⊆ C := Set.singleton_subset_iff.mpr hx
+  have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
   exact Set.mem_mem_imp_pair_subset hxs hxys
 
 /-- ### Exercise 5.1
@@ -317,23 +222,20 @@ theorem exercise_5_5b {A : Set α} (B : Set β)
 
 If `⟨x, y⟩ ∈ A`, then `x` and `y` belong to `⋃ ⋃ A`.
 -/
-theorem theorem_3d {A : Set (Set (Set (α ⊕ α)))} (h : OrderedPair x y ∈ A)
-  : Sum.inl x ∈ ⋃₀ (⋃₀ A) ∧ Sum.inr y ∈ ⋃₀ (⋃₀ A) := by
-  have hp : OrderedPair x y ⊆ ⋃₀ A := Chapter_2.exercise_3_3 (OrderedPair x y) h
-  have hp' : ∀ t, t ∈ {{Sum.inl x}, {Sum.inl x, Sum.inr y}} → t ∈ ⋃₀ A := hp
-
-  have hq := hp' {Sum.inl x, Sum.inr y} (by simp)
-  have hq' := Chapter_2.exercise_3_3 {Sum.inl x, Sum.inr y} hq
-
-  have : ∀ t, t ∈ {Sum.inl x, Sum.inr y} → t ∈ ⋃₀ (⋃₀ A) := hq'
-  exact ⟨this (Sum.inl x) (by simp), this (Sum.inr y) (by simp)⟩
+theorem theorem_3d {A : Set (Set (Set α))} (h : OrderedPair x y ∈ A)
+  : x ∈ ⋃₀ (⋃₀ A) ∧ y ∈ ⋃₀ (⋃₀ A) := by
+  have hp := Chapter_2.exercise_3_3 (OrderedPair x y) h
+  unfold OrderedPair at hp  
+  have hq : {x, y} ∈ ⋃₀ A := hp (by simp)
+  have : {x, y} ⊆ ⋃₀ ⋃₀ A := Chapter_2.exercise_3_3 {x, y} hq
+  exact ⟨this (by simp), this (by simp)⟩
 
 /-- ### Exercise 6.6
 
 Show that a set `A` is a relation **iff** `A ⊆ dom A × ran A`.
 -/
-theorem exercise_6_6 {A : Set (α × β)}
-  : A ⊆ Set.prod (Prod.fst '' A) (Prod.snd '' A) := by
+theorem exercise_6_6 {A : Set.Relation α}
+  : A ⊆ Set.prod (A.dom) (A.ran) := by
   show ∀ t, t ∈ A → t ∈ Set.prod (Prod.fst '' A) (Prod.snd '' A)
   intro (a, b) ht
   unfold Set.prod
@@ -346,4 +248,85 @@ theorem exercise_6_6 {A : Set (α × β)}
   ]
   exact ⟨⟨b, ht⟩, ⟨a, ht⟩⟩
 
+/-- ### Exercise 6.7
+
+Show that if `R` is a relation, then `fld R = ⋃ ⋃ R`.
+-/
+theorem exercise_6_7 {R : Set.Relation α}
+  : R.fld = ⋃₀ ⋃₀ R.toOrderedPairs := by
+  let img := R.toOrderedPairs
+  suffices R.fld ⊆ ⋃₀ ⋃₀ img ∧ ⋃₀ ⋃₀ img ⊆ R.fld from
+    Set.Subset.antisymm_iff.mpr this
+
+  apply And.intro
+  · show ∀ x, x ∈ R.fld → x ∈ ⋃₀ ⋃₀ img
+    intro x hx
+    apply Or.elim hx
+    · intro hd
+      unfold Set.Relation.dom Prod.fst at hd
+      simp only [
+        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
+        unfold Set.image
+        simp only [Prod.exists, Set.mem_setOf_eq]
+        exact ⟨x, ⟨y, ⟨hp, rfl⟩⟩⟩
+      unfold OrderedPair at hm
+      have : {x} ∈ ⋃₀ img := Chapter_2.exercise_3_3 {{x}, {x, y}} hm (by simp)
+      exact (Chapter_2.exercise_3_3 {x} this) (show x ∈ {x} by rfl)
+    · intro hr
+      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
+        simp only [Set.mem_image, Prod.exists]
+        exact ⟨t, ⟨x, ⟨ht, rfl⟩⟩⟩
+      unfold OrderedPair at hm
+      have : {t, x} ∈ ⋃₀ img := Chapter_2.exercise_3_3 {{t}, {t, x}} hm
+        (show {t, x} ∈ {{t}, {t, x}} by simp)
+      exact Chapter_2.exercise_3_3 {t, x} this (show x ∈ {t, x} by simp)
+
+  · show ∀ t, t ∈ ⋃₀ ⋃₀ img → t ∈ Set.Relation.fld R
+    intro t ht
+    have ⟨T, hT⟩ : ∃ T ∈ ⋃₀ img, t ∈ T := ht
+    have ⟨T', hT'⟩ : ∃ T' ∈ img, T ∈ T' := hT.left
+    dsimp at hT'
+    unfold Set.Relation.toOrderedPairs at hT'
+    simp only [Set.mem_image, Prod.exists] at hT'
+    have ⟨x, ⟨y, ⟨p, hp⟩⟩⟩ := hT'.left
+    have hr := hT'.right
+    rw [← hp] at hr
+    unfold OrderedPair at hr
+    simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at hr
+
+    -- Use `exercise_6_6` to prove that if `t = x` then `t ∈ dom R` and if
+    -- `t = y` then `t ∈ ran R`.
+    have hxy_mem : t = x ∨ t = y → t ∈ Set.Relation.fld R := by
+      intro ht
+      have hz : R ⊆ Set.prod (R.dom) (R.ran) := exercise_6_6
+      have : (x, y) ∈ Set.prod (R.dom) (R.ran) := hz p
+      unfold Set.prod at this
+      simp at this
+      apply Or.elim ht
+      · intro ht'
+        rw [← ht'] at this
+        exact Or.inl this.left
+      · intro ht'
+        rw [← ht'] at this
+        exact Or.inr this.right
+
+    -- Eliminate `T = {x} ∨ T = {x, y}`.
+    apply Or.elim hr
+    · intro hx
+      have := hT.right
+      rw [hx] at this
+      simp only [Set.mem_singleton_iff] at this
+      exact hxy_mem (Or.inl this)
+    · intro hxy
+      have := hT.right
+      rw [hxy] at this
+      simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at this
+      exact hxy_mem this
+
 end Enderton.Set.Chapter_3

Common/Set.lean

@@ -1,3 +1,5 @@
 import Common.Set.Basic
 import Common.Set.Interval
+import Common.Set.OrderedPair
 import Common.Set.Partition
+import Common.Set.Relation

Common/Set/Basic.lean

@@ -1,7 +1,6 @@
-import Mathlib.Data.Set.Basic
-import Mathlib.SetTheory.ZFC.Basic
-
 import Common.Logic.Basic
+import Mathlib.Data.Set.Basic
+import Mathlib.Data.Set.Prod
 
 /-! # Common.Set.Basic
 

Common/Set/OrderedPair.lean

@@ -0,0 +1,119 @@
+import Common.Set.Basic
+
+/-! # Ordered Pairs
+
+A representation of an ordered pair in basic set theory. Like `Set`, it is
+assumed an ordered pair is homogeneous.
+-/
+
+/--
+Kazimierz Kuratowski's definition of an ordered pair.
+-/
+def OrderedPair (x y : α) : Set (Set α) := {{x}, {x, y}}
+
+namespace OrderedPair
+
+/--
+For any sets `x`, `y`, `u`, and `v`, `⟨u, v⟩ = ⟨x, y⟩` **iff** `u = x ∧ v = y`.
+-/
+theorem ext_iff {x y u v : α}
+  : (OrderedPair x y = OrderedPair u v) ↔ (x = u ∧ y = v) := by
+  unfold OrderedPair
+  apply Iff.intro
+  · intro h
+    have hu := Set.ext_iff.mp h {u}
+    have huv := Set.ext_iff.mp h {u, v}
+    simp only [
+      Set.mem_singleton_iff, Set.mem_insert_iff, true_or, or_true, iff_true
+    ] at hu huv
+    apply Or.elim hu <;> apply Or.elim huv
+
+    · -- #### Case 1
+      -- `{u} = {x}` and `{u, v} = {x}`.
+      intro huv_x hu_x
+      rw [Set.singleton_eq_singleton_iff] at hu_x
+      rw [hu_x] at huv_x
+      have hx_v := Set.pair_eq_singleton_mem_imp_eq_self huv_x
+      rw [hu_x, hx_v] at h
+      simp only [Set.mem_singleton_iff, Set.insert_eq_of_mem] at h
+      have := Set.pair_eq_singleton_mem_imp_eq_self $
+        Set.pair_eq_singleton_mem_imp_eq_self h
+      rw [← hx_v] at this
+      exact ⟨hu_x.symm, this⟩
+
+    · -- #### Case 2
+      -- `{u} = {x}` and `{u, v} = {x, y}`.
+      intro huv_xy hu_x
+      rw [Set.singleton_eq_singleton_iff] at hu_x
+      rw [hu_x] at huv_xy
+      by_cases hx_v : x = v
+      · rw [hx_v] at huv_xy
+        simp only [Set.mem_singleton_iff, Set.insert_eq_of_mem] at huv_xy
+        have := Set.pair_eq_singleton_mem_imp_eq_self huv_xy.symm
+        exact ⟨hu_x.symm, this⟩
+      · rw [Set.ext_iff] at huv_xy
+        have := huv_xy v
+        simp only [
+          Set.mem_singleton_iff, Set.mem_insert_iff, or_true, true_iff
+        ] at this
+        exact ⟨hu_x.symm, Or.elim this (absurd ·.symm hx_v) (·.symm)⟩
+
+    · -- #### Case 3
+      -- `{u} = {x, y}` and `{u, v} = {x}`.
+      intro huv_x hu_xy
+      rw [Set.ext_iff] at huv_x hu_xy
+      have hu_x := huv_x u
+      have hy_u := hu_xy y
+      simp only [
+        Set.mem_singleton_iff,
+        Set.mem_insert_iff,
+        true_or,
+        true_iff,
+        or_true,
+        iff_true
+      ] at hu_x hy_u 
+      apply Or.elim huv
+      · intro huv_x
+        rw [← hu_x, Set.ext_iff] at huv_x
+        have := huv_x v
+        simp only [
+          Set.mem_singleton_iff, Set.mem_insert_iff, or_true, true_iff
+        ] at this
+        exact ⟨hu_x.symm, by rwa [this]⟩
+      · intro huv_xy
+        rw [hu_x, Set.ext_iff] at huv_xy
+        have := huv_xy v
+        simp only [
+          Set.mem_singleton_iff, Set.mem_insert_iff, or_true, true_iff
+         ] at this
+        apply Or.elim this
+        · intro hv_x
+          rw [hy_u, hu_x]
+          exact ⟨rfl, hv_x.symm⟩
+        · intro hv_y
+          exact ⟨hu_x.symm, hv_y.symm⟩
+
+    · -- #### Case 4
+      -- `{u} = {x, y}` and `{u, v} = {x, y}`.
+      intro huv_xy hu_xy
+      rw [Set.ext_iff] at huv_xy hu_xy
+      have hx_u := hu_xy x
+      have hy_u := hu_xy y
+      simp only [
+        Set.mem_singleton_iff, Set.mem_insert_iff, true_or, iff_true, or_true
+      ] at hx_u hy_u 
+      have := huv_xy v
+      simp only [
+        Set.mem_singleton_iff, Set.mem_insert_iff, or_true, true_iff
+      ] at this 
+      apply Or.elim this
+      · intro hv_x
+        rw [hv_x, hx_u]
+        exact ⟨rfl, hy_u⟩
+      · intro hv_y
+        exact ⟨hx_u, hv_y.symm⟩
+
+  · intro h
+    rw [h.left, h.right]
+
+end OrderedPair

Common/Set/Relation.lean

@@ -0,0 +1,48 @@
+import Common.Set.OrderedPair
+import Mathlib.Data.Set.Basic
+import Mathlib.Data.Set.Prod
+
+/-! # Relations
+
+A representation of a relation, i.e. a set of ordered pairs. Like `Set`, it is
+assumed a relation is homogeneous.
+-/
+
+namespace Set
+
+/--
+A relation type as defined by Enderton.
+
+We choose to use tuples to represent our ordered pairs, as opposed to
+Kuratowski's definition of a set.
+
+Not to be confused with the Lean-provided `Rel`.
+-/
+abbrev Relation (α : Type _) := Set (α × α)
+
+namespace Relation
+
+/--
+The domain of a `Relation`.
+-/
+def dom (R : Relation α) : Set α := Prod.fst '' R
+
+/--
+The range of a `Relation`.
+-/
+def ran (R : Relation α) : Set α := Prod.snd '' R
+
+/--
+The field of a `Relation`.
+-/
+def fld (R : Relation α) : Set α := dom R ∪ ran 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)
+
+end Relation
+
+end Set