From 27372eb16053c1eba2ac276eecbfa5c41e00ad10 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 23 Jun 2023 15:47:55 -0600 Subject: [PATCH] Enderton. Add additional definitions and prove Theorem 3E. --- Bookshelf/Enderton/Set.tex | 53 ++++++++++-- Bookshelf/Enderton/Set/Chapter_3.lean | 118 ++++++++++++++++++++++---- Common/Set/Relation.lean | 42 ++++++++- 3 files changed, 189 insertions(+), 24 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 5038562..56d34bf 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/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} diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 769f25d..4c4e025 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/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₂⟩⟩ - exact ⟨b, ⟨h₂.left, ⟨h₁, h₂.right⟩⟩⟩ - · intro ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩ - exact ⟨h₂, ⟨b, ⟨h₁, h₃⟩⟩⟩ + · intro ⟨h₁, b, h₂⟩ + exact ⟨b, h₂.left, h₁, h₂.right⟩ + · intro ⟨b, h₁, 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₃⟩⟩⟩ - exact ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩ - · intro ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩ - exact ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩ + · intro ⟨b, h₁, h₂, h₃⟩ + exact ⟨b, h₁, h₂, h₃⟩ + · intro ⟨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⟩⟩⟩ - exact ⟨t, ⟨ht, ⟨y, hx⟩⟩⟩ - · intro ⟨t, ⟨ht, ⟨y, hx⟩⟩⟩ - exact ⟨y, ⟨t, ⟨ht, hx⟩⟩⟩ + · intro ⟨y, t, ht, hx⟩ + exact ⟨t, ht, y, hx⟩ + · intro ⟨t, ht, y, 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 \ No newline at end of file diff --git a/Common/Set/Relation.lean b/Common/Set/Relation.lean index ae0d219..f06d893 100644 --- a/Common/Set/Relation.lean +++ b/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