diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 1d14456..b1d81a1 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -3037,14 +3037,14 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive \statementpadding - \lean*{Bookshelf/Enderton/Set/Chapter\_3} - {Enderton.Set.Chapter\_3.theorem\_3e\_i} + \lean*{Common/Set/Relation} + {Set.Relation.dom\_inv\_eq\_ran\_self} - \lean*{Bookshelf/Enderton/Set/Chapter\_3} - {Enderton.Set.Chapter\_3.theorem\_3e\_ii} + \lean*{Common/Set/Relation} + {Set.Relation.ran\_inv\_eq\_dom\_self} - \lean{Bookshelf/Enderton/Set/Chapter\_3} - {Enderton.Set.Chapter\_3.theorem\_3e\_iii} + \lean{Common/Set/Relation} + {Set.Relation.inv\_inv\_eq\_self} We prove that (i) $\dom{(F^{-1})} = \ran{F}$, (ii) $\ran{(F^{-1})} = \dom{F}$, and (iii) $(F^{-1})^{-1} = F$. @@ -3081,7 +3081,7 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive \end{proof} -\subsection{\partial{Theorem 3F}}% +\subsection{\verified{Theorem 3F}}% \label{sub:theorem-3f} \begin{theorem}[3F] @@ -3095,11 +3095,11 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive \statementpadding - \lean*{Bookshelf/Enderton/Set/Chapter\_3} - {Enderton.Set.Chapter\_3.theorem\_3f\_i} + \lean*{Common/Set/Relation} + {Set.Relation.single\_valued\_inv\_iff\_single\_rooted\_self} - \lean{Bookshelf/Enderton/Set/Chapter\_3} - {Enderton.Set.Chapter\_3.theorem\_3f\_ii} + \lean{Common/Set/Relation} + {Set.Relation.single\_valued\_self\_iff\_single\_rooted\_inv} We prove that (i) any set $F$, $F^{-1}$ is a function iff $F$ is single-rooted and (ii) any relation $F$ is a function iff $F^{-1}$ is @@ -3151,14 +3151,16 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive \end{proof} -\subsection{\partial{Lemma 1}}% +\subsection{\verified{Lemma 1}}% \label{sub:lemma-1} -Assume that $F$ is a one-to-one function. -Then $F^{-1}$ is a one-to-one function. +For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \begin{proof} + \lean{Common/Set/Relation} + {Set.Relation.one\_to\_one\_self\_iff\_one\_to\_one\_inv} + We prove that (i) $F^{-1}$ is a function and (ii) $F^{-1}$ is single-rooted. \paragraph{(i)}% @@ -3211,11 +3213,11 @@ Then $F^{-1}$ is a one-to-one function. For all $x \in \dom{F}$, $\left< x, F(x) \right> \in F$. Then $\left< F(x), x \right> \in F^{-1}$. - Since $F^{-1}$ is single-valued, $F^{-1}(F(x)) = x$ is well-defined. + Since $F^{-1}$ is single-valued, $F^{-1}(F(x)) = x$. For all $y \in \ran{F}$, $\left< y, F^{-1}(y) \right> \in F^{-1}$. Then $\left< F^{-1}(y), y \right> \in F$. - Since $F$ is single-valued, $F(F^{-1}(y)) = y$ is also well-defined. + Since $F$ is single-valued, $F(F^{-1}(y)) = y$. \end{proof} diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 4c4e025..b2d87b5 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -432,86 +432,22 @@ theorem exercise_6_9_ii {A : Set (Set.Relation α)} intro _ y hy R hR exact ⟨y, hy R hR⟩ -/-- ### Theorem 3E (i) +/-- ### Theorem 3G (i) -For a set `F`, `dom F⁻¹ = ran F`. +Assume that `F` is a one-to-one function. If `x ∈ dom F`, then `F⁻¹(F(x)) = x`. -/ -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 +theorem theorem_3g_i {F : Set.Relation α} + (hF : Set.Relation.isOneToOne F) (hx : x ∈ F.dom) + : ∃! y, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by sorry -/-- ### Theorem 3F (ii) +/-- ### Theorem 3G (ii) -For a relation `F`, `F` is a function **iff** `F⁻¹` is single-rooted. +Assume that `F` is a one-to-one function. If `y ∈ ran F`, then `F(F⁻¹(y)) = y`. -/ -theorem theorem_3f_ii {F : Set.Relation α} - : Set.Relation.isSingleValued F ↔ Set.Relation.isSingleRooted F.inv := by +theorem theorem_3g_ii {F : Set.Relation α} + (hF : Set.Relation.isOneToOne F) (hy : x ∈ F.ran) + : ∃! x, (x, y) ∈ F ∧ (y, x) ∈ 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 f06d893..0812f52 100644 --- a/Common/Set/Relation.lean +++ b/Common/Set/Relation.lean @@ -22,16 +22,52 @@ abbrev Relation (α : Type _) := Set (α × α) namespace Relation +/-! ## Domain and Range -/ + /-- The domain of a `Relation`. -/ def dom (R : Relation α) : Set α := Prod.fst '' R +/-- +The first component of any pair in a `Relation` must be a member of the +`Relation`'s domain. +-/ +theorem mem_pair_imp_fst_mem_dom {R : Relation α} (h : (x, y) ∈ R) + : x ∈ dom R := by + unfold dom Prod.fst + simp only [mem_image, Prod.exists, exists_and_right, exists_eq_right] + exact ⟨y, h⟩ + +/-- +If `x ∈ dom R`, there exists some `y` such that `⟨x, y⟩ ∈ R`. +-/ +theorem dom_exists {R : Relation α} (hx : x ∈ R.dom) + : ∃ y, (x, y) ∈ R := by + unfold dom at hx + simp only [mem_image, Prod.exists, exists_and_right, exists_eq_right] at hx + exact hx + /-- The range of a `Relation`. -/ def ran (R : Relation α) : Set α := Prod.snd '' R +theorem mem_pair_imp_snd_mem_ran {R : Relation α} (h : (x, y) ∈ R) + : y ∈ ran R := by + unfold ran Prod.snd + simp only [mem_image, Prod.exists, exists_eq_right] + exact ⟨x, h⟩ + +/-- +If `x ∈ ran R`, there exists some `t` such that `⟨t, x⟩ ∈ R`. +-/ +theorem ran_exists {R : Relation α} (hx : x ∈ R.ran) + : ∃ t, (t, x) ∈ R := by + unfold ran at hx + simp only [mem_image, Prod.exists, exists_eq_right] at hx + exact hx + /-- The field of a `Relation`. -/ @@ -42,24 +78,113 @@ The inverse of a `Relation`. -/ def inv (R : Relation α) : Relation α := { (p.2, p.1) | p ∈ R } +/-- +`(x, y)` is a member of relation `R` **iff** `(y, x)` is a member of `R⁻¹`. +-/ +@[simp] +theorem mem_self_comm_mem_inv {R : Relation α} + : (y, x) ∈ R.inv ↔ (x, y) ∈ R := by + unfold inv + simp only [Prod.exists, mem_setOf_eq, Prod.mk.injEq] + apply Iff.intro + · intro ⟨x', y', hxy⟩ + rw [← hxy.right.left, ← hxy.right.right] + exact hxy.left + · intro hxy + exact ⟨x, y, hxy, rfl, rfl⟩ + +/-- +The inverse of the inverse of a `Relation` is the `Relation`. +-/ +@[simp] +theorem inv_inv_eq_self (R : Relation α) + : R.inv.inv = R := 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 + +/-- +For a set `F`, `dom F⁻¹ = ran F`. +-/ +@[simp] +theorem dom_inv_eq_ran_self {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⟩ + +/-- +For a set `F`, `ran F⁻¹ = dom F`. +-/ +@[simp] +theorem ran_inv_eq_dom_self {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⟩ + +/-! ## Composition -/ + /-- The composition of two `Relation`s. -/ def comp (F G : Relation α) : Relation α := { p | ∃ t, (p.1, t) ∈ G ∧ (t, p.2) ∈ F} +/-! ## Restriction -/ + /-- The restriction of a `Relation` to a `Set`. -/ def restriction (R : Relation α) (A : Set α) : Relation α := { p ∈ R | p.1 ∈ A } +/-! ## Image -/ + /-- The image of a `Relation` under a `Set`. -/ def image (R : Relation α) (A : Set α) : Set α := { y | ∃ u ∈ A, (u, y) ∈ R } +/-! ## Single-Rooted and Single-Valued -/ + /-- 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`. @@ -76,6 +201,72 @@ 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 +/-- +For a set `F`, `F⁻¹` is a function **iff** `F` is single-rooted. +-/ +theorem single_valued_inv_iff_single_rooted_self {F : Set.Relation α} + : isSingleValued F.inv ↔ isSingleRooted F := by + apply Iff.intro + · intro hF + unfold isSingleValued at hF + simp only [ + dom_inv_eq_ran_self, + ran_inv_eq_dom_self, + mem_self_comm_mem_inv + ] at hF + suffices ∀ x ∈ F.ran, ∃! y, (y, x) ∈ F from hF + intro x hx + have ⟨y, hy⟩ := hF x hx + simp only [ + ran_inv_eq_dom_self, + mem_self_comm_mem_inv, + and_imp + ] at hy + refine ⟨y, hy.left.right, ?_⟩ + intro y₁ hy₁ + exact hy.right y₁ (mem_pair_imp_fst_mem_dom hy₁) hy₁ + · intro hF + unfold isSingleRooted at hF + unfold isSingleValued + simp only [ + dom_inv_eq_ran_self, + ran_inv_eq_dom_self, + mem_self_comm_mem_inv + ] + exact hF + +/-- +For a relation `F`, `F` is a function **iff** `F⁻¹` is single-rooted. +-/ +theorem single_valued_self_iff_single_rooted_inv {F : Set.Relation α} + : Set.Relation.isSingleValued F ↔ Set.Relation.isSingleRooted F.inv := by + conv => lhs; rw [← inv_inv_eq_self F] + rw [single_valued_inv_iff_single_rooted_self] + +/-- +A `Relation` `R` is one-to-one if it is a single-rooted function. +-/ +def isOneToOne (R : Relation α) : Prop := + isSingleValued R ∧ isSingleRooted R + +/-- +A `Relation` is one-to-one **iff** it's inverse is. +-/ +theorem one_to_one_self_iff_one_to_one_inv {R : Relation α} + : isOneToOne R ↔ isOneToOne R.inv := by + unfold isOneToOne isSingleValued isSingleRooted + conv => rhs; simp only [ + dom_inv_eq_ran_self, + ran_inv_eq_dom_self, + mem_self_comm_mem_inv, + eq_iff_iff + ] + apply Iff.intro <;> + · intro ⟨hx, hy⟩ + exact ⟨hy, hx⟩ + +/-! ## Ordered Pairs -/ + /-- Convert a `Relation` into an equivalent representation using `OrderedPair`s. -/