diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index c120ae0..7170cb0 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -2363,4 +2363,114 @@ If not, then under what conditions does equality hold? \end{proof} +\section{Exercises 5}% +\label{sec:exercises-5} + +\subsection{\verified{Exercise 5.1}}% +\label{sub:exercise-5.1} + +Suppose that we attempted to generalize the Kuratowski definitions of ordered + pairs to ordered triples by defining + $$\left< x, y, z \right>^* = \{\{x\}, \{x, y\}, \{x, y, z\}\}.$$ +Show that this definition is unsuccessful by giving examples of objects + $u$, $v$, $w$, $x$, $y$, $z$ with + $\left< x, y, z \right>^* = \left< u, v, w \right>^*$ but with either + $y \neq v$ or $z \neq w$ (or both). + +\begin{proof} + + \lean{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.exercise\_5\_1} + + Let $x = 1$, $y = 1$, and $z = 2$. + Let $u = 1$, $v = 2$, and $w = 2$. + Then + \begin{align*} + \left< x, y, z \right>^* + & = \{\{x\}, \{x, y\}, \{x, y, z\}\} \\ + & = \{\{1\}, \{1, 1\}, \{1, 1, 2\}\} \\ + & = \{\{1\}, \{1, 2\}\}. + \end{align*} + Likewise + \begin{align*} + \left< u, v, w \right>^* + & = \{\{u\}, \{u, v\}, \{u, v, w\}\} \\ + & = \{\{1\}, \{1, 2\}, \{1, 2, 2\}\} \\ + & = \{\{1\}, \{1, 2\}\}. + \end{align*} + Thus $\left< x, y, z \right>^* = \left< u, v, w \right>^*$ but $y \neq v$. + +\end{proof} + +\subsection{\verified{Exercise 5.2a}}% +\label{sub:exercise-5.2a} + +Show that $A \times (B \cup C) = (A \times B) \cup (A \times C)$. + +\begin{proof} + + \lean{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.exercise\_5\_2a} + + Let $A$, $B$, and $C$ be arbitrary sets. + Then by definition of the \nameref{sub:cartesian-product} and union of sets, + \begin{align*} + A \times (B \cup C) + & = \{ \left< x, y \right> \mid x \in A \land y \in (B \cup C) \} \\ + & = \{ \left< x, y \right> \mid + x \in A \land (y \in B \lor y \in C) \} \\ + & = \{ \left< x, y \right> \mid + (x \in A \land y \in B) \lor (x \in A \land y \in C) \} \\ + & = \{ \left< x, y \right> \mid (x \in A \land y \in B) \} \cup + \{ \left< x, y \right> \mid (x \in A \land y \in C) \} \\ + & = (A \times B) \cup (A \times C). + \end{align*} + +\end{proof} + +\subsection{\verified{Exercise 5.2b}}% +\label{sub:exercise-5.2b} + +Show that if $A \times B = A \times C$ and $A \neq \emptyset$, then $B = C$. + +\begin{proof} + + \lean{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.exercise\_5\_2b} + + Let $A$, $B$, and $C$ be arbitrary sets such that $A \neq \emptyset$. + By definition of the \nameref{sub:cartesian-product}, + \begin{align} + A \times B & = \{ \left< x, y \right> \mid x \in A \land y \in B \} + & \label{sub:exercise-5.2b-eq1} \\ + A \times C & = \{ \left< x, y \right> \mid x \in A \land y \in C \}. + & \label{sub:exercise-5.2b-eq2} + \end{align} + There are two cases to consider: + + \paragraph{Case 1}% + + Suppose $B \neq \emptyset$. + Then $A \times B \neq \emptyset$ and $A \times C \neq \emptyset$. + Let $\left< x, y \right> \in A \times B$. + By \eqref{sub:exercise-5.2b-eq1}, $x \in A$ and $y \in B$. + By the \nameref{ref:extensionality-axiom}, + $$\left< x, y \right> \in A \times B \iff \left< x, y \right> \in A \times C.$$ + Therefore $\left< x, y \right> \in A \times C$. + By \eqref{sub:exercise-5.2b-eq2}, $x \in A$ and $y \in C$. + Since membership of $y$ in $B$ and in $C$ holds biconditionally, the + \nameref{ref:extensionality-axiom} indicates $B = C$. + + \paragraph{Case 2}% + + Suppose $B = \emptyset$. + Then there is no $\left< x, y \right>$ such that $x \in A$ and $y \in B$. + Thus $A \times B = \emptyset$ and $A \times C = \emptyset$. + But then there cannot exist an $\left< x, y \right>$ such that $x \in A$ + and $y \in C$ either. + Since $A \neq \emptyset$, it must be the case that $C = \emptyset$. + Thus $B = C$. + +\end{proof} + \end{document} diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 809dfce..f337111 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -1,6 +1,7 @@ import Mathlib.Data.Set.Basic import Mathlib.SetTheory.ZFC.Basic +import Common.Set.Basic import Common.Set.OrderedPair /-! # Enderton.Chapter_3 @@ -19,4 +20,71 @@ theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C) 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 + +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}}. +``` +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` +or `z ≠ w` (or both). +-/ +theorem exercise_5_1 {x y z u v w : ℕ} + (hx : x = 1) (hy : y = 1) (hz : z = 2) + (hu : u = 1) (hv : v = 2) (hw : w = 2) + : ({{x}, {x, y}, {x, y, z}} : Set (Set ℕ)) = {{u}, {u, v}, {u, v, w}} + ∧ y ≠ v := by + apply And.intro + · rw [hx, hy, hz, hu, hv, hw] + simp + · rw [hy, hv] + simp only + +/-- ### Exercise 5.2a + +Show that `A × (B ∪ C) = (A × B) ∪ (A × C)`. +-/ +theorem exercise_5_2a {A B C : Set α} + : Set.prod A (B ∪ C) = (Set.prod A B) ∪ (Set.prod A C) := by + calc Set.prod A (B ∪ C) + _ = { p | p.1 ∈ A ∧ p.2 ∈ B ∪ C } := rfl + _ = { p | p.1 ∈ A ∧ (p.2 ∈ B ∨ p.2 ∈ C) } := rfl + _ = { p | (p.1 ∈ A ∧ p.2 ∈ B) ∨ (p.1 ∈ A ∧ p.2 ∈ C) } := by + ext x + rw [Set.mem_setOf_eq] + conv => lhs; rw [and_or_left] + _ = { p | p ∈ Set.prod A B ∨ (p ∈ Set.prod A C) } := rfl + _ = (Set.prod A B) ∪ (Set.prod A C) := rfl + +/-- ### Exercise 5.2b + +Show that if `A × B = A × C` and `A ≠ ∅`, then `B = C`. +-/ +theorem exercise_5_2b {A B C : Set α} + (h : Set.prod A B = Set.prod A C) (hA : Set.Nonempty A) + : B = C := by + by_cases hB : Set.Nonempty B + · suffices B ⊆ C ∧ C ⊆ B from Set.Subset.antisymm_iff.mpr this + have ⟨a, ha⟩ := hA + apply And.intro + · show ∀ t, t ∈ B → t ∈ C + intro t ht + have : (a, t) ∈ Set.prod A B := ⟨ha, ht⟩ + rw [h] at this + exact this.right + · show ∀ t, t ∈ C → t ∈ B + intro t ht + have : (a, t) ∈ Set.prod A C := ⟨ha, ht⟩ + rw [← h] at this + exact this.right + · have nB : B = ∅ := Set.not_nonempty_iff_eq_empty.mp hB + rw [nB, Set.prod_right_emptyset_eq_emptyset, Set.ext_iff] at h + rw [nB] + by_contra nC + have ⟨a, ha⟩ := hA + have ⟨c, hc⟩ := Set.nonempty_iff_ne_empty.mpr (Ne.symm nC) + exact (h (a, c)).mpr ⟨ha, hc⟩ + end Enderton.Set.Chapter_3 \ No newline at end of file diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index 18c2ce2..61dd742 100644 --- a/Common/Set/Basic.lean +++ b/Common/Set/Basic.lean @@ -1,4 +1,5 @@ import Mathlib.Data.Set.Basic +import Mathlib.SetTheory.ZFC.Basic import Common.Logic.Basic @@ -128,6 +129,42 @@ Every `Set` is a member of its own powerset. theorem self_mem_powerset_self {A : Set α} : A ∈ 𝒫 A := subset_self A +/-! ## Cartesian Product -/ + +/-- +For any `Set` `A`, `∅ × A = ∅`. +-/ +theorem prod_left_emptyset_eq_emptyset {A : Set α} + : Set.prod (∅ : Set α) A = ∅ := by + unfold prod + simp only [mem_empty_iff_false, false_and, setOf_false] + +/-- +For any `Set` `A`, `A × ∅ = ∅`. +-/ +theorem prod_right_emptyset_eq_emptyset {A : Set α} + : Set.prod A (∅ : Set α) = ∅ := by + unfold prod + simp only [mem_empty_iff_false, and_false, setOf_false] + +/-- +For any `Set`s `A` and `B`, if both `A` and `B` are nonempty, then `A × B` is +also nonempty. +-/ +theorem prod_nonempty_nonempty_imp_nonempty_prod {A B : Set α} + : A ≠ ∅ ∧ B ≠ ∅ ↔ Set.prod A B ≠ ∅ := by + apply Iff.intro + · intro nAB h + have ⟨a, ha⟩ := nonempty_iff_ne_empty.mpr nAB.left + have ⟨b, hb⟩ := nonempty_iff_ne_empty.mpr nAB.right + rw [Set.ext_iff] at h + exact (h (a, b)).mp ⟨ha, hb⟩ + · intro h + rw [← nonempty_iff_ne_empty] at h + have ⟨(a, b), ⟨ha, hb⟩⟩ := h + rw [← nonempty_iff_ne_empty, ← nonempty_iff_ne_empty] + exact ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ + /-! ## Symmetric Difference -/ /--