From 931e617161c90c4a9a8bd6a5b292867d34b4c1a8 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 26 Jun 2023 07:08:25 -0600 Subject: [PATCH] Enderton. Formally verify theorem 3G. --- Bookshelf/Enderton/Set.tex | 10 +++++++- Bookshelf/Enderton/Set/Chapter_3.lean | 20 ++++++++++++---- Common/Set/Relation.lean | 34 +++++++++++++++++++++++++-- 3 files changed, 56 insertions(+), 8 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 95923b8..a1dfdc0 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -3194,7 +3194,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \end{proof} -\subsection{\partial{Theorem 3G}}% +\subsection{\verified{Theorem 3G}}% \label{sub:theorem-3g} \begin{theorem}[3G] @@ -3207,6 +3207,14 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \begin{proof} + \statementpadding + + \lean*{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.theorem\_3g\_i} + + \lean{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.theorem\_3g\_ii} + Suppose $F$ is a one-to-one \nameref{ref:function}. Then \nameref{sub:lemma-1} indicates $F^{-1}$ is a one-to-one function with domain $\ran{F}$ and range $\dom{F}$. diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index b2d87b5..008d8af 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -436,18 +436,28 @@ 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 {F : Set.Relation α} - (hF : Set.Relation.isOneToOne F) (hx : x ∈ F.dom) +theorem theorem_3g_i {α : Type _} {x y : α} {F : Set.Relation α} + (hF : Set.Relation.isOneToOne F) (hx : x ∈ Set.Relation.dom F) : ∃! y, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by - sorry + simp only [Set.Relation.mem_self_comm_mem_inv, and_self] + have ⟨y, hy⟩ := Set.Relation.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 /-- ### 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 : x ∈ F.ran) + (hF : Set.Relation.isOneToOne F) (hy : y ∈ F.ran) : ∃! x, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by - sorry + simp only [Set.Relation.mem_self_comm_mem_inv, and_self] + have ⟨x, hx⟩ := Set.Relation.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 end Enderton.Set.Chapter_3 \ No newline at end of file diff --git a/Common/Set/Relation.lean b/Common/Set/Relation.lean index 0812f52..11a7124 100644 --- a/Common/Set/Relation.lean +++ b/Common/Set/Relation.lean @@ -43,7 +43,7 @@ theorem mem_pair_imp_fst_mem_dom {R : Relation α} (h : (x, y) ∈ R) 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 + : ∃ 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 @@ -63,7 +63,7 @@ theorem mem_pair_imp_snd_mem_ran {R : Relation α} (h : (x, y) ∈ R) 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 + : ∃ t : α, (t, x) ∈ R := by unfold ran at hx simp only [mem_image, Prod.exists, exists_eq_right] at hx exact hx @@ -192,6 +192,21 @@ 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 single-rooted `Relation` should map the same output to the same input. +-/ +theorem single_rooted_eq_unique {R : Relation α} {x₁ x₂ y : α} + (hR : isSingleRooted R) + : (x₁, y) ∈ R → (x₂, y) ∈ R → x₁ = x₂ := by + intro hx₁ hx₂ + unfold isSingleRooted at hR + have := hR y (mem_pair_imp_snd_mem_ran hx₁) + have ⟨y₁, hy₁⟩ := this + simp only [and_imp] at hy₁ + have h₁ := hy₁.right x₁ (mem_pair_imp_fst_mem_dom hx₁) hx₁ + have h₂ := hy₁.right x₂ (mem_pair_imp_fst_mem_dom hx₂) hx₂ + rw [h₁, h₂] + /-- 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`. @@ -201,6 +216,21 @@ 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 +/-- +A single-valued `Relation` should map the same input to the same output. +-/ +theorem single_valued_eq_unique {R : Relation α} {x y₁ y₂ : α} + (hR : isSingleValued R) + : (x, y₁) ∈ R → (x, y₂) ∈ R → y₁ = y₂ := by + intro hy₁ hy₂ + unfold isSingleValued at hR + have := hR x (mem_pair_imp_fst_mem_dom hy₁) + have ⟨x₁, hx₁⟩ := this + simp only [and_imp] at hx₁ + have h₁ := hx₁.right y₁ (mem_pair_imp_snd_mem_ran hy₁) hy₁ + have h₂ := hx₁.right y₂ (mem_pair_imp_snd_mem_ran hy₂) hy₂ + rw [h₁, h₂] + /-- For a set `F`, `F⁻¹` is a function **iff** `F` is single-rooted. -/