From f5d1fc546a78874434b354fb019a834f14bf4115 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 10 Jun 2023 16:01:23 -0600 Subject: [PATCH] Enderton. Move Kuratowski's definition of an ordered pair into chapter; not likely to be used outside this book. --- Bookshelf/Enderton/Set.tex | 55 ++++++--- Bookshelf/Enderton/Set/Chapter_3.lean | 157 ++++++++++++++++++++++++-- Common/Set.lean | 1 - Common/Set/OrderedPair.lean | 98 ---------------- 4 files changed, 189 insertions(+), 122 deletions(-) delete mode 100644 Common/Set/OrderedPair.lean diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 218c4bf..f9bed8a 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -2244,7 +2244,8 @@ If not, then under what conditions does equality hold? \begin{proof} - \lean{Common/Set/OrderedPair}{Set.OrderedPair.ext\_iff} + \lean{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.OrderedPair.ext\_iff} Let $x$, $y$, $u$, and $v$ be arbitrary sets. @@ -2518,7 +2519,7 @@ Show that there is no set to which every ordered pair belongs. \end{proof} -\subsection{\partial{Exercise 5.5a}}% +\subsection{\unverified{Exercise 5.5a}}% \label{sub:exercise-5.5a} Assume that $A$ and $B$ are given sets, and show that there exists a set $C$ @@ -2581,32 +2582,54 @@ In other words, show that $\{\{x\} \times B \mid x \in A\}$ is a set. \end{proof} -\subsection{\partial{Exercise 5.5b}}% +\subsection{\verified{Exercise 5.5b}}% \label{sub:exercise-5.5b} With $A$, $B$, and $C$ as above, show that $A \times B = \bigcup C$. \begin{proof} + \lean{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.exercise\_5\_5b} + Let $A$ and $B$ be arbitrary sets. We want to show that \begin{equation} \label{sub:exercise-5.5b-eq1} A \times B = \bigcup\; \{\{x\} \times B \mid x \in A\}. \end{equation} - Note that \nameref{sub:cartesian-product} and \nameref{sub:exercise-5.5a} - prove the left- and right-hand sides of \eqref{sub:exercise-5.5b-eq1} are - sets respectively. - Then - \begin{align*} - A \times B - & = \{ y \mid \exists x \in A, \exists b \in B, y = \left< x, b \right> \} \\ - & = \{ y \mid \exists b \in B, \exists x \in A, y = \left< x, b \right> \} \\ - & = \{ y \mid \exists b \in B, y \in \{ \left< x, b \right> \mid x \in A \} \} \\ - & = \{ y \mid y \in \{ \left< x, b \right> \mid x \in A \land b \in B \} \} \\ - & = \{ y \mid \exists z \in \{\{x\} \times B \mid x \in A \}, y \in z \} \\ - & = \bigcup \{\{x\} \times B \mid x \in A \}. - \end{align*} + The left-hand side of \eqref{sub:exercise-5.5b-eq1} is a set by virtue of + \nameref{sub:cartesian-product}. + The right-hand side of \eqref{sub:exercise-5.5b-eq1} is a set by virtue of + \nameref{sub:exercise-5.5a}. + We prove the set on each side is a subset of the other. + + \paragraph{($\subseteq$)}% + + Let $c \in A \times B$. + Then there exists some $a \in A$ and $b \in B$ such that + $c = \left< a, b \right>$. + Thus $c \in \{a\} \times B$. + We also note $\{a\} \times B \in \{\{x\} \times B \mid x \in A\}$, + specifically when $x = a$. + Therefore, by the \nameref{ref:union-axiom}, + $c \in \bigcup\;\{\{x\} \times B \mid x \in A\}$. + + \paragraph{($\supseteq$)}% + + Let $c \in \bigcup\; \{\{x\} \times B \mid x \in A\}$. + By the \nameref{ref:union-axiom}, there exists some + $b \in \{\{x\} \times B \mid x \in A\}$ such that $c \in b$. + Then there exists some $x \in A$ such that $b = \{x\} \times B$. + Therefore $c \in \{x\} \times B$. + But $x \in A$ meaning $c \in A \times B$ as well. + + \paragraph{Conclusion}% + + Since we have shown + $A \times B \subseteq \bigcup\; \{\{x\} \times B \mid x \in A\}$ and + $A \times B \supseteq \bigcup\; \{\{x\} \times B \mid x \in A\}$, it + follows \eqref{sub:exercise-5.5b-eq1} is a true identity. \end{proof} diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 06adea4..92f3154 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -1,8 +1,7 @@ import Mathlib.Data.Set.Basic -import Mathlib.SetTheory.ZFC.Basic +import Common.Logic.Basic import Common.Set.Basic -import Common.Set.OrderedPair /-! # Enderton.Chapter_3 @@ -11,13 +10,107 @@ 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 : x ∈ C) (hy : y ∈ C) - : Set.OrderedPair x y ∈ 𝒫 𝒫 C := by - have hxs : {x} ⊆ C := Set.singleton_subset_iff.mpr hx - have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy +theorem theorem_3b {C : Set (α ⊕ α)} (hx : Sum.inl x ∈ C) (hy : Sum.inr 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 exact Set.mem_mem_imp_pair_subset hxs hxys /-- ### Exercise 5.1 @@ -25,7 +118,8 @@ theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C) Suppose that we attempted to generalize the Kuratowski definitions of ordered pairs to ordered triples by defining ``` -⟨x, y, z⟩* = {{x}, {x, y}, {x, y, z}}. +⟨x, y, z⟩* = {{x}, {x, y}, {x, y, z}}.open Set + ``` Show that this definition is unsuccessful by giving examples of objects `u`, `v`, `w`, `x`, `y`, `z` with `⟨x, y, z⟩* = ⟨u, v, w⟩*` but with either `y ≠ v` @@ -115,4 +209,53 @@ theorem exercise_5_3 {A : Set (Set α)} {𝓑 : Set (Set β)} · intro ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩ exact ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩ +/-- ### Exercise 5.5a + +Assume that `A` and `B` are given sets, and show that there exists a set `C` +such that for any `y`, +``` +y ∈ C ↔ y = {x} × B for some x in A. +``` +In other words, show that `{{x} × B | x ∈ A}` is a set. +-/ +theorem exercise_5_5a {A : Set α} {B : Set β} + : ∃ C : Set (Set (α × β)), + y ∈ C ↔ ∃ x ∈ A, y = Set.prod {x} B := by + sorry + +/-- ### Exercise 5.5b + +With `A`, `B`, and `C` as above, show that `A × B = ∪ C`. +-/ +theorem exercise_5_5b {A : Set α} (B : Set β) + : Set.prod A B = ⋃₀ {Set.prod ({x} : Set α) B | x ∈ A} := by + suffices Set.prod A B ⊆ ⋃₀ {Set.prod {x} B | x ∈ A} ∧ + ⋃₀ {Set.prod {x} B | x ∈ A} ⊆ Set.prod A B from + Set.Subset.antisymm_iff.mpr this + apply And.intro + · show ∀ t, t ∈ Set.prod A B → t ∈ ⋃₀ {Set.prod {x} B | x ∈ A} + intro t h + simp only [Set.mem_setOf_eq] at h + unfold Set.sUnion sSup Set.instSupSetSet + simp only [Set.mem_setOf_eq, exists_exists_and_eq_and] + unfold Set.prod at h + simp only [Set.mem_setOf_eq] at h + refine ⟨t.fst, ⟨h.left, ?_⟩⟩ + unfold Set.prod + simp only [Set.mem_singleton_iff, Set.mem_setOf_eq, true_and] + exact h.right + · show ∀ t, t ∈ ⋃₀ {Set.prod {x} B | x ∈ A} → t ∈ Set.prod A B + unfold Set.prod + intro t ht + simp only [ + Set.mem_singleton_iff, + Set.mem_sUnion, + Set.mem_setOf_eq, + exists_exists_and_eq_and + ] at ht + have ⟨a, ⟨h, ⟨ha, hb⟩⟩⟩ := ht + simp only [Set.mem_setOf_eq] + rw [← ha] at h + exact ⟨h, hb⟩ + end Enderton.Set.Chapter_3 \ No newline at end of file diff --git a/Common/Set.lean b/Common/Set.lean index b611e08..ae92e76 100644 --- a/Common/Set.lean +++ b/Common/Set.lean @@ -1,4 +1,3 @@ import Common.Set.Basic import Common.Set.Interval -import Common.Set.OrderedPair import Common.Set.Partition \ No newline at end of file diff --git a/Common/Set/OrderedPair.lean b/Common/Set/OrderedPair.lean deleted file mode 100644 index 497b184..0000000 --- a/Common/Set/OrderedPair.lean +++ /dev/null @@ -1,98 +0,0 @@ -import Mathlib.Data.Set.Basic - -import Common.Logic.Basic -import Common.Set.Basic - -namespace Set - -/-- -Kazimierz Kuratowski's definition of an ordered pair. - -Like `Set`, this is a homogeneous structure. --/ -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 - : (OrderedPair x y = OrderedPair u v) ↔ (x = u ∧ y = v) := by - unfold OrderedPair - apply Iff.intro - · intro h - have h' := h - rw [Set.ext_iff] at h' - have hu := h' {u} - have huv := h' {u, v} - simp only [mem_singleton_iff, mem_insert_iff, true_or, iff_true] at hu - simp only [mem_singleton_iff, 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 [singleton_eq_singleton_iff] at hu_x - rw [hu_x] at huv_x - have hx_v := pair_eq_singleton_mem_imp_eq_self huv_x - rw [hu_x, hx_v] at h - simp only [mem_singleton_iff, insert_eq_of_mem] at h - have := pair_eq_singleton_mem_imp_eq_self $ - 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 [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 at huv_xy - have := 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 at this - apply Or.elim this - · intro hv_x - rw [hu_x, ← hv_x] at h - simp at h - have := pair_eq_singleton_mem_imp_eq_self $ - pair_eq_singleton_mem_imp_eq_self h - exact ⟨hu_x.symm, this⟩ - · intro hv_y - exact ⟨hu_x.symm, hv_y.symm⟩ - · apply Or.elim huv - · -- #### Case 3 - -- `{u} = {x, y}` and `{u, v} = {x}`. - intro huv_x hu_xy - rw [Set.ext_iff] at huv_x - have hu_x := huv_x u - have hv_x := huv_x v - simp only [mem_singleton_iff, mem_insert_iff, true_or, true_iff] at hu_x - simp only [mem_singleton_iff, mem_insert_iff, or_true, true_iff] at hv_x - rw [← hu_x] at hu_xy - have := pair_eq_singleton_mem_imp_eq_self hu_xy.symm - rw [hu_x, ← hv_x] at this - exact ⟨hu_x.symm, this⟩ - · -- #### Case 4 - -- `{u} = {x, y}` and `{u, v} = {x, y}`. - intro huv_xy hu_xy - rw [Set.ext_iff] at hu_xy - have hx_u := hu_xy x - have hy_u := hu_xy y - simp only [mem_singleton_iff, mem_insert_iff, true_or, iff_true] at hx_u - simp only [mem_singleton_iff, mem_insert_iff, or_true, iff_true] at hy_u - rw [hx_u, hy_u] at huv_xy - simp only [mem_singleton_iff, insert_eq_of_mem] at huv_xy - have := pair_eq_singleton_mem_imp_eq_self huv_xy - rw [← this] at hy_u - exact ⟨hx_u, hy_u⟩ - · intro h - rw [h.left, h.right] - -end OrderedPair - -end Set \ No newline at end of file