From 8b5736397c7bec4bbca933d0213ffd643cccb0d5 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 20 Jun 2023 15:02:09 -0600 Subject: [PATCH] Enderton. Break out relations/ordered pairs. Exercise 6.7. --- Bookshelf/Enderton/Set.tex | 5 +- Bookshelf/Enderton/Set/Chapter_2.lean | 2 +- Bookshelf/Enderton/Set/Chapter_3.lean | 207 ++++++++++++-------------- Common/Set.lean | 4 +- Common/Set/Basic.lean | 5 +- Common/Set/OrderedPair.lean | 119 +++++++++++++++ Common/Set/Relation.lean | 48 ++++++ 7 files changed, 272 insertions(+), 118 deletions(-) create mode 100644 Common/Set/OrderedPair.lean create mode 100644 Common/Set/Relation.lean diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index d0e7400..cf527a2 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/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}$. diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean index b37dd43..7baa685 100644 --- a/Bookshelf/Enderton/Set/Chapter_2.lean +++ b/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 diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index c079bc7..8fe6ec3 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/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 \ No newline at end of file diff --git a/Common/Set.lean b/Common/Set.lean index ae92e76..76ba02f 100644 --- a/Common/Set.lean +++ b/Common/Set.lean @@ -1,3 +1,5 @@ import Common.Set.Basic import Common.Set.Interval -import Common.Set.Partition \ No newline at end of file +import Common.Set.OrderedPair +import Common.Set.Partition +import Common.Set.Relation \ No newline at end of file diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index 0e5fdfb..d138f04 100644 --- a/Common/Set/Basic.lean +++ b/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 diff --git a/Common/Set/OrderedPair.lean b/Common/Set/OrderedPair.lean new file mode 100644 index 0000000..f7236e2 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/Common/Set/Relation.lean b/Common/Set/Relation.lean new file mode 100644 index 0000000..ae0d219 --- /dev/null +++ b/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 \ No newline at end of file