Enderton. Theorem 3H and helper theorems.

Bookshelf/Enderton/Set.tex

@@ -3229,7 +3229,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \end{proof}
 
-\subsection{\partial{Theorem 3H}}%
+\subsection{\verified{Theorem 3H}}%
 \label{sub:theorem-3h}
 
 \begin{theorem}[3H]
@@ -3246,6 +3246,14 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \begin{proof}
 
+  \statementpadding
+
+  \lean*{Common/Set/Relation}
+    {Set.Relation.single\_valued\_comp\_is\_single\_valued}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3h\_dom}
+
   Let $F$ and $G$ be \nameref{ref:function}s.
   By definition of the \nameref{ref:composition} of $F$ and $G$,
     \begin{equation}

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -291,7 +291,7 @@ theorem exercise_6_7 {R : Set.Relation α}
     intro t ht
     have ⟨T, hT⟩ : ∃ T ∈ ⋃₀ img, t ∈ T := ht
     have ⟨T', hT'⟩ : ∃ T' ∈ img, T ∈ T' := hT.left
-    dsimp at hT'
+    dsimp only at hT'
     unfold Set.Relation.toOrderedPairs at hT'
     simp only [Set.mem_image, Prod.exists] at hT'
     have ⟨x, ⟨y, ⟨p, hp⟩⟩⟩ := hT'.left
@@ -329,6 +329,10 @@ theorem exercise_6_7 {R : Set.Relation α}
       simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at this
       exact hxy_mem this
 
+section
+
+open Set.Relation
+
 /-- ### Exercise 6.8 (i)
 
 Show that for any set `𝓐`:
@@ -337,9 +341,9 @@ dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
 ```
 -/
 theorem exercise_6_8_i {A : Set (Set.Relation α)}
-  : Set.Relation.dom (⋃₀ A) = ⋃₀ { Set.Relation.dom R | R ∈ A } := by
+  : dom (⋃₀ A) = ⋃₀ { dom R | R ∈ A } := by
   ext x
-  unfold Set.Relation.dom Prod.fst
+  unfold dom Prod.fst
   simp only [
     Set.mem_image,
     Set.mem_sUnion,
@@ -363,9 +367,9 @@ ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
 ```
 -/
 theorem exercise_6_8_ii {A : Set (Set.Relation α)}
-  : Set.Relation.ran (⋃₀ A) = ⋃₀ { Set.Relation.ran R | R ∈ A } := by
+  : ran (⋃₀ A) = ⋃₀ { ran R | R ∈ A } := by
   ext x
-  unfold Set.Relation.ran Prod.snd
+  unfold ran Prod.snd
   simp only [
     Set.mem_image,
     Set.mem_sUnion,
@@ -389,9 +393,9 @@ dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
 ```
 -/
 theorem exercise_6_9_i {A : Set (Set.Relation α)}
-  : Set.Relation.dom (⋂₀ A) ⊆ ⋂₀ { Set.Relation.dom R | R ∈ A } := by
-  show ∀ x, x ∈ Set.Relation.dom (⋂₀ A) → x ∈ ⋂₀ { Set.Relation.dom R | R ∈ A }
-  unfold Set.Relation.dom Prod.fst
+  : dom (⋂₀ A) ⊆ ⋂₀ { dom R | R ∈ A } := by
+  show ∀ x, x ∈ dom (⋂₀ A) → x ∈ ⋂₀ { dom R | R ∈ A }
+  unfold dom Prod.fst
   simp only [
     Set.mem_image,
     Set.mem_sInter,
@@ -415,9 +419,9 @@ ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
 ```
 -/
 theorem exercise_6_9_ii {A : Set (Set.Relation α)}
-  : Set.Relation.ran (⋂₀ A) ⊆ ⋂₀ { Set.Relation.ran R | R ∈ A } := by
-  show ∀ x, x ∈ Set.Relation.ran (⋂₀ A) → x ∈ ⋂₀ { Set.Relation.ran R | R ∈ A }
-  unfold Set.Relation.ran Prod.snd
+  : ran (⋂₀ A) ⊆ ⋂₀ { ran R | R ∈ A } := by
+  show ∀ x, x ∈ ran (⋂₀ A) → x ∈ ⋂₀ { ran R | R ∈ A }
+  unfold ran Prod.snd
   simp only [
     Set.mem_image,
     Set.mem_sInter,
@@ -437,27 +441,70 @@ theorem exercise_6_9_ii {A : Set (Set.Relation α)}
 Assume that `F` is a one-to-one function. If `x ∈ dom F`, then `F⁻¹(F(x)) = x`.
 -/
 theorem theorem_3g_i {α : Type _} {x y : α} {F : Set.Relation α}
-  (hF : Set.Relation.isOneToOne F) (hx : x ∈ Set.Relation.dom F)
+  (hF : isOneToOne F) (hx : x ∈ dom F)
   : ∃! y, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by
-  simp only [Set.Relation.mem_self_comm_mem_inv, and_self]
-  have ⟨y, hy⟩ := Set.Relation.dom_exists hx
+  simp only [mem_self_comm_mem_inv, and_self]
+  have ⟨y, hy⟩ := dom_exists hx
   refine ⟨y, hy, ?_⟩
   intro y₁ hy₁
-  unfold Set.Relation.isOneToOne at hF
-  exact (Set.Relation.single_valued_eq_unique hF.left hy hy₁).symm
+  unfold isOneToOne at hF
+  exact (single_valued_eq_unique hF.left hy hy₁).symm
 
 /-- ### Theorem 3G (ii)
 
 Assume that `F` is a one-to-one function. If `y ∈ ran F`, then `F(F⁻¹(y)) = y`.
 -/
 theorem theorem_3g_ii {F : Set.Relation α}
-  (hF : Set.Relation.isOneToOne F) (hy : y ∈ F.ran)
+  (hF : isOneToOne F) (hy : y ∈ F.ran)
   : ∃! x, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by
-  simp only [Set.Relation.mem_self_comm_mem_inv, and_self]
-  have ⟨x, hx⟩ := Set.Relation.ran_exists hy
+  simp only [mem_self_comm_mem_inv, and_self]
+  have ⟨x, hx⟩ := ran_exists hy
   refine ⟨x, hx, ?_⟩
   intro x₁ hx₁
-  unfold Set.Relation.isOneToOne at hF
-  exact (Set.Relation.single_rooted_eq_unique hF.right hx hx₁).symm
+  unfold isOneToOne at hF
+  exact (single_rooted_eq_unique hF.right hx hx₁).symm
+
+/-- ### Theorem 3H
+
+Assume that `F` and `G` are functions. Then
+```
+dom (F ∘ G) = {x ∈ dom G | G(x) ∈ dom F}.
+```
+-/
+theorem theorem_3h_dom {F G : Set.Relation α}
+  (_ : isSingleValued F) (hG : isSingleValued G)
+  : dom (comp F G) = {x ∈ dom G | ∃! y, (x, y) ∈ G ∧ y ∈ dom F } := by
+  let rhs := {x ∈ dom G | ∃! y, (x, y) ∈ G ∧ y ∈ dom F }
+  suffices dom (comp F G) ⊆ rhs ∧ rhs ⊆ dom (comp F G) from
+    Set.Subset.antisymm_iff.mpr this
+  apply And.intro
+  · show ∀ t, t ∈ dom (comp F G) → t ∈ rhs
+    intro t ht
+    simp only [Set.mem_setOf_eq]
+    have ⟨z, hz⟩ := dom_exists ht
+    refine ⟨dom_comp_imp_dom_self ht, ?_⟩
+    simp only [Set.mem_setOf_eq] at hz
+    have ⟨a, ha⟩ := hz
+    unfold dom
+    simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right]
+    unfold ExistsUnique
+    simp only [and_imp, forall_exists_index]
+    refine ⟨a, ⟨ha.left, z, ha.right⟩, ?_⟩
+    intro y₁ hy₁
+    exact fun _ _ => single_valued_eq_unique hG hy₁ ha.left
+  · show ∀ t, t ∈ rhs → t ∈ dom (comp F G)
+    intro t ht
+    simp only [Set.mem_setOf_eq] at ht
+    unfold dom
+    simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right]
+    have ⟨a, ha⟩ := ht.right
+    simp at ha
+    have ⟨b, hb⟩ := dom_exists ha.left.right
+    refine ⟨b, ?_⟩
+    unfold comp
+    simp only [Set.mem_setOf_eq]
+    exact ⟨a, ha.left.left, hb⟩
+
+end
 
 end Enderton.Set.Chapter_3

Common/Set/Relation.lean

@@ -159,14 +159,6 @@ theorem ran_inv_eq_dom_self {F : Set.Relation α}
   · intro ⟨y, hy⟩
     exact ⟨y, x, y, hy, rfl, rfl⟩
 
-/-! ## Composition -/
-
-/--
-The composition of two `Relation`s.
--/
-def comp (F G : Relation α) : Relation α :=
-  { p | ∃ t, (p.1, t) ∈ G ∧ (t, p.2) ∈ F}
-
 /-! ## Restriction -/
 
 /--
@@ -295,6 +287,84 @@ theorem one_to_one_self_iff_one_to_one_inv {R : Relation α}
   · intro ⟨hx, hy⟩
     exact ⟨hy, hx⟩
 
+
+/-! ## Composition -/
+
+/--
+The composition of two `Relation`s.
+-/
+def comp (F G : Relation α) : Relation α :=
+  { p | ∃ t : α, (p.1, t) ∈ G ∧ (t, p.2) ∈ F}
+
+/--
+If `x ∈ dom (F ∘ G)`, then `x ∈ dom G`.
+-/
+theorem dom_comp_imp_dom_self {F G : Relation α}
+  : x ∈ dom (comp F G) → x ∈ dom G := by
+  unfold dom comp
+  simp only [
+    mem_image,
+    mem_setOf_eq,
+    Prod.exists,
+    exists_and_right,
+    exists_eq_right,
+    forall_exists_index
+  ]
+  intro y t ht
+  exact ⟨t, ht.left⟩
+
+/--
+If `y ∈ ran (F ∘ G)`, then `y ∈ ran F`.
+-/
+theorem ran_comp_imp_ran_self {F G : Relation α}
+  : y ∈ ran (comp F G) → y ∈ ran F := by
+  unfold ran comp
+  simp only [
+    mem_image,
+    mem_setOf_eq,
+    Prod.exists,
+    exists_eq_right,
+    forall_exists_index
+  ]
+  intro x t ht
+  exact ⟨t, ht.right⟩
+
+/--
+The composition of two functions is itself a function.
+-/
+theorem single_valued_comp_is_single_valued {F G : Relation α}
+  (hF : isSingleValued F) (hG : isSingleValued G)
+  : isSingleValued (comp F G) := by
+  unfold isSingleValued
+  intro x hx
+  have ⟨y, hxy⟩ := dom_exists hx
+  have hy := mem_pair_imp_snd_mem_ran hxy
+  refine ⟨y, ⟨hy, hxy⟩, ?_⟩
+  simp only [and_imp]
+
+  intro y₁ _ hxy₁
+  unfold comp at hxy hxy₁
+  simp only [mem_setOf_eq] at hxy hxy₁
+  have ⟨t₁, ht₁⟩ := hxy
+  have ⟨t₂, ht₂⟩ := hxy₁
+
+  -- First show `t₁ = t₂` and then show `y = y₁`.
+  have t_eq : t₁ = t₂ := by
+    unfold isSingleValued at hG
+    have ⟨t', ht'⟩ := hG x (mem_pair_imp_fst_mem_dom ht₁.left)
+    simp only [and_imp] at ht'
+    have ht₁' := ht'.right t₁ (mem_pair_imp_snd_mem_ran ht₁.left) ht₁.left
+    have ht₂' := ht'.right t₂ (mem_pair_imp_snd_mem_ran ht₂.left) ht₂.left
+    rw [ht₁', ht₂']
+
+  unfold isSingleValued at hF
+  rw [t_eq] at ht₁
+  have ⟨y', hy'⟩ := hF t₂ (mem_pair_imp_fst_mem_dom ht₁.right)
+  simp only [and_imp] at hy'
+  have hk₁ := hy'.right y (mem_pair_imp_snd_mem_ran ht₁.right) ht₁.right
+  have hk₂ := hy'.right y₁ (mem_pair_imp_snd_mem_ran ht₂.right) ht₂.right
+  rw [hk₁, hk₂]
+
 /-! ## Ordered Pairs -/
 
 /--