From 8279131d742e9a2814a0dc75c86b53ba6016c54d Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sun, 21 May 2023 18:32:59 -0600 Subject: [PATCH] Enderton, basic axioms/unions exercises. --- Bookshelf/Enderton/Set.tex | 291 +++++++++++++++++++++++--- Bookshelf/Enderton/Set/Chapter_1.lean | 276 +++++++++++++++++++++++- Common/Set/Basic.lean | 55 ++++- preamble.tex | 5 +- 4 files changed, 586 insertions(+), 41 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 336862c..7c5074c 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -432,7 +432,7 @@ List all the members of $V_4$. \section{Exercises 3}% \label{sec:exercises-3} -\subsection{\unverified{Exercise 3.1}}% +\subsection{\verified{Exercise 3.1}}% \label{sub:exercise-3.1} Assume that $A$ is the set of integers divisible by $4$. @@ -440,25 +440,31 @@ Similarly assume that $B$ and $C$ are the sets of integers divisible by $9$ and $10$, respectively. What is in $A \cap B \cap C$? -\begin{proof} +\begin{answer} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_1} -\end{proof} + The set of integers divisible by $4$, $9$, and $10$. -\subsection{\unverified{Exercise 3.2}}% +\end{answer} + +\subsection{\verified{Exercise 3.2}}% \label{sub:exercise-3.2} Give an example of sets $A$ and $B$ for which $\bigcup A = \bigcup B$ but $A \neq B$. -\begin{proof} +\begin{answer} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_2} -\end{proof} + Let $A = \{\{1\}, \{2\}\}$ and $B = \{\{1, 2\}\}$. -\subsection{\unverified{Exercise 3.3}}% +\end{answer} + +\subsection{\verified{Exercise 3.3}}% \label{sub:exercise-3.3} Show that every member of a set $A$ is a subset of $\bigcup A$. @@ -466,22 +472,38 @@ Show that every member of a set $A$ is a subset of $\bigcup A$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_3} + + Let $x \in A$. + By definition, $$\bigcup A = \{ y \mid (\exists b \in A) y \in b\}.$$ + Then $\{ y \mid y \in x\} \subseteq \bigcup A$. + But $\{ y \mid y \in x\} = x$. + Thus $x \subseteq \bigcup A$. \end{proof} -\subsection{\unverified{Exercise 3.4}}% +\subsection{\verified{Exercise 3.4}}% \label{sub:exercise-3.4} Show that if $A \subseteq B$, then $\bigcup A \subseteq \bigcup B$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_4} + + Let $A$ and $B$ be sets such that $A \subseteq B$. + Let $x \in \bigcup A$. + By definition of the union, there exists some $b \in A$ such that $x \in b$. + By definition of the subset, $b \in B$. + This immediatley implies $x \in \bigcup B$. + Since this holds for all $x \in \bigcup A$, it follows + $\bigcup A \subseteq \bigcup B$. \end{proof} -\subsection{\unverified{Exercise 3.5}}% +\subsection{\verified{Exercise 3.5}}% \label{sub:exercise-3.5} Assume that every member of $\mathscr{A}$ is a subset of $B$. @@ -489,22 +511,61 @@ Show that $\bigcup \mathscr{A} \subseteq B$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_5} + + Let $x \in \bigcup \mathscr{A}$. + By definition, + $$\bigcup \mathscr{A} = \{ y \mid (\exists b \in A)y \in b \}.$$ + Then there exists some $b \in A$ such that $x \in b$. + By hypothesis, $b \subseteq B$. + Thus $x$ must also be a member of $B$. + Since this holds for all $x \in \bigcup \mathscr{A}$, it follows + $\bigcup \mathscr{A} \subseteq B$. \end{proof} -\subsection{\unverified{Exercise 3.6a}}% +\subsection{\verified{Exercise 3.6a}}% \label{sub:exercise-3.6a} Show that for any set $A$, $\bigcup \powerset{A} = A$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_6a} + + We prove that (i) $\bigcup \powerset{A} \subseteq A$ and (ii) + $A \subseteq \bigcup \powerset{A}$. + + \paragraph{(i)}% + \label{par:exercise-3.6a-i} + + By definition, the \nameref{ref:power-set} of $A$ is the set of all subsets + of $A$. + In other words, every member of $\powerset{A}$ is a subset of $A$. + By \nameref{sub:exercise-3.5}, $\bigcup \powerset{A} \subseteq A$. + + \paragraph{(ii)}% + \label{par:exercise-3.6a-ii} + + Let $x \in A$. + By definition of the power set of $A$, $\{x\} \in \powerset{A}$. + By definition of the union, + $$\bigcup \powerset{A} = + \{ y \mid (\exists b \in \powerset{A}), y \in b).$$ + Since $x \in \{x\}$ and $\{x\} \in \powerset{A}$, it follows + $x \in \bigcup \powerset{A}$. + Thus $A \subseteq \bigcup \powerset{A}$. + + \paragraph{Conclusion}% + + By \nameref{par:exercise-3.6a-i} and \nameref{par:exercise-3.6a-ii}, + $\bigcup \powerset{A} = A$. \end{proof} -\subsection{\unverified{Exercise 3.6b}}% +\subsection{\verified{Exercise 3.6b}}% \label{sub:exercise-3.6b} Show that $A \subseteq \powerset{\bigcup A}$. @@ -512,35 +573,176 @@ Under what conditions does equality hold? \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_6b} + + Let $x \in A$. + By \nameref{sub:exercise-3.3}, $x$ is a subset of $\bigcup A$. + By the definition of the \nameref{ref:power-set}, + $$\powerset{\bigcup A} = \{ y \mid y \subseteq \bigcup A \}.$$ + Therefore $x \in \powerset{\bigcup A}$. + Since this holds for all $x \in A$, $A \subseteq \powerset{\bigcup A}$. + + \suitdivider + + We show equality holds if and only if there exists some set $B$ such that + $A = \powerset{B}$. + + \paragraph{($\Rightarrow$)}% + \label{par:exercise-3.6b-right} + + Suppose $A = \powerset{\bigcup A}$. + Then our statement immediately follows by settings $B = \bigcup A$. + + \paragraph{($\Leftarrow$)}% + \label{par:exercise-3.6b-left} + + Suppose there exists some set $B$ such that $A = \powerset{B}$. + Therefore + \begin{align*} + \powerset{\bigcup A} + & = \powerset{\left(\bigcup {\powerset {B}}\right)} \\ + & = \powerset{B} & \textref{sub:exercise-3.6a} \\ + & = A. + \end{align*} + + \paragraph{Conclusion}% + + By \nameref{par:exercise-3.6b-right} and \nameref{par:exercise-3.6b-left}, + $A = \powerset{\bigcup A}$ if and only if there exists some set $B$ such + that $A = \powerset{B}$. \end{proof} -\subsection{\unverified{Exercise 3.7a}}% +\subsection{\verified{Exercise 3.7a}}% \label{sub:exercise-3.7a} Show that for any sets $A$ and $B$, - $$\powerset{A} \cap \powerset{B} = \powerset(A \cap B).$$ + $$\powerset{A} \cap \powerset{B} = \powerset{(A \cap B)}.$$ \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_7a} + + Let $A$ and $B$ be arbitrary sets. We show that + $\powerset{A} \cap \powerset{B} \subseteq \powerset{(A \cap B)}$ and then + show that $\powerset{A} \cap \powerset{B} \supseteq \powerset{(A \cap B)}$. + + \paragraph{($\subseteq$)}% + + Let $x \in \powerset{A} \cap \powerset{B}$. + That is, $x \in \powerset{A}$ and $x \in \powerset{B}$. + By the definition of the \nameref{ref:power-set}, + \begin{align*} + \powerset{A} & = \{ y \mid y \subseteq A \} \\ + \powerset{B} & = \{ y \mid y \subseteq B \} + \end{align*} + Thus $x \subseteq A$ and $x \subseteq B$, meaning $x \subseteq A \cap B$. + But then $x \in \powerset{(A \cap B)}$, the set of all subsets of + $A \cap B$. + Since this holds for all $x \in \powerset{A} \cap \powerset{B}$, it follows + $$\powerset{A} \cap \powerset{B} \subseteq \powerset{(A \cap B)}.$$ + + \paragraph{($\supseteq$)}% + + Let $x \in \powerset{(A \cap B)}$. + By the definition of the \nameref{ref:power-set}, + $$\powerset{(A \cap B)} = \{ y \mid y \subseteq A \cap B \}.$$ + Thus $x \subseteq A \cap B$, meaning $x \subseteq A$ and $x \subseteq B$. + But this implies $x \in \powerset{A}$, the set of all subsets of $A$. + Likewise $x \in \powerset{B}$, the set of all subsets of $B$. + Thus $x \in \powerset{A} \cap \powerset{B}$. + Since this holds for all $x \in \powerset{(A \cap B)}$, it follows + $$\powerset{(A \cap B)} \subseteq \powerset{A} \cap \powerset{B}.$$ + + \paragraph{Conclusion}% + + Since each side of our identity is a subset of the other, + $$\powerset{(A \cap B)} = \powerset{A} \cap \powerset{B}.$$ \end{proof} -\subsection{\unverified{Exercise 3.7b}}% +\subsection{\verified{Exercise 3.7b}}% \label{sub:exercise-3.7b} -Show that $\powerset{A} \cup \powerset{B} \subseteq \powerset(A \cup B)$. +Show that $\powerset{A} \cup \powerset{B} \subseteq \powerset{(A \cup B)}$. Under what conditions does equality hold? \begin{proof} - TODO + \ % Add space. + + \lean*{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_7b\_i} + + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_7b\_ii} + + Let $x \in \powerset{A} \cup \powerset{B}$. + By definition, $x \in \powerset{A}$ or $x \in \powerset{B}$ (or both). + By the definition of the \nameref{ref:power-set}, + \begin{align*} + \powerset{A} &= \{ y \mid y \subseteq A \} \\ + \powerset{B} &= \{ y \mid y \subseteq B \}. + \end{align*} + Thus $x \subseteq A$ or $x \subseteq B$. + Therefore $x \subseteq A \cup B$. + But then $x \in \powerset{(A \cup B)}$, the set of all subsets of $A \cup B$. + + \suitdivider + + We show equality holds if and only if one of $A$ or $B$ is a subset of the + other. + + \paragraph{($\Rightarrow$)}% + \label{par:exercise-3.7b-right} + + Suppose + \begin{equation} + \label{sub:exercise-3.7b-eq1} + \powerset{A} \cup \powerset{B} = \powerset{(A \cup B)}. + \end{equation} + By the definition of the \nameref{ref:power-set}, + $A \cup B \in \powerset{(A \cup B)}$. + Then \eqref{sub:exercise-3.7b-eq1} implies + $A \cup B \in \powerset{A} \cup \powerset{B}$. + That is, $A \cup B \in \powerset{A}$ or $A \cup B \in \powerset{B}$ (or + both). + + For the sake of contradiction, suppose $A \not\subseteq B$ and + $B \not\subseteq A$. + Then there exists an element $x \in A$ such that $x \not\in B$ and there + exists an element $y \in B$ such that $y \not\in A$. + But then $A \cup B \not\in \powerset{A}$ since $y$ cannot be a member of a + member of $\powerset{A}$. + Likewise, $A \cup B \not\in \powerset{B}$ since $x$ cannot be a member of a + member of $\powerset{B}$. + Therefore our assumption is incorrect. + In other words, $A \subseteq B$ or $B \subseteq A$. + + \paragraph{($\Leftarrow$)}% + \label{par:exercise-3.7b-left} + + WLOG, suppose $A \subseteq B$. + Then, by \nameref{sub:exercise-1.3}, $\powerset{A} \subseteq \powerset{B}$. + Thus + \begin{align*} + \powerset{A} \cup \powerset{B} + & = \powerset{B} \\ + & = \powerset{A \cup B}. + \end{align*} + + \paragraph{Conclusion}% + + By \nameref{par:exercise-3.7b-right} and \nameref{par:exercise-3.7b-left}, + it follows + $\powerset{A} \cup \powerset{B} \subseteq \powerset{(A \cup B)}$ if and + only if $A \subseteq B$ or $B \subseteq A$. \end{proof} -\subsection{\unverified{Exercise 3.8}}% +\subsection{\partial{Exercise 3.8}}% \label{sub:exercise-3.8} Show that there is no set to which every singleton (that is, every set of the @@ -550,23 +752,37 @@ Show that there is no set to which every singleton (that is, every set of the \begin{proof} - TODO + We proceed by contradiction. + Suppose there existed a set $A$ consisting of every singleton. + Then the \nameref{ref:union-axiom} suggests $\bigcup A$ is a set. + But this set is precisely the class of all sets, which is \textit{not} a set. + Thus our original assumption was incorrect. + That is, there is no set to which every singleton belongs. \end{proof} -\subsection{\unverified{Exercise 3.9}}% +\subsection{\verified{Exercise 3.9}}% \label{sub:exercise-3.9} Give an example of sets $a$ and $B$ for which $a \in B$ but - $\powerset{A} \not\in \powerset{B}$. + $\powerset{a} \not\in \powerset{B}$. -\begin{proof} +\begin{answer} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_9} -\end{proof} + Let $a = \{1\}$ and $B = \{\{1\}\}$. + Then + \begin{align*} + \powerset{a} & = \{\emptyset, \{1\}\} \\ + \powerset{B} & = \{\emptyset, \{\{1\}\}\}. + \end{align*} + It immediately follows that $\powerset{a} \not\in \powerset{B}$. -\subsection{\unverified{Exercise 3.10}}% +\end{answer} + +\subsection{\verified{Exercise 3.10}}% \label{sub:exercise-3.10} Show that if $a \in B$, then $\powerset{a} \in \powerset{\powerset{\bigcup B}}$. @@ -574,7 +790,16 @@ Show that if $a \in B$, then $\powerset{a} \in \powerset{\powerset{\bigcup B}}$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Chapter\_1} + {Enderton.Set.Chapter\_1.exercise\_3\_10} + + Suppose $a \in B$. + By \nameref{sub:exercise-3.3}, $a \subseteq \bigcup B$. + By \nameref{sub:exercise-1.3}, $\powerset{a} \subseteq \powerset{\bigcup B}$. + By the definition of the \nameref{ref:power-set}, + $$\powerset{\powerset{\bigcup B}} = + \{ y \mid y \subseteq \powerset{\bigcup B} \}.$$ + Therefore $\powerset{a} \in \powerset{\powerset{\bigcup B}}$. \end{proof} diff --git a/Bookshelf/Enderton/Set/Chapter_1.lean b/Bookshelf/Enderton/Set/Chapter_1.lean index bc79def..996ac5c 100644 --- a/Bookshelf/Enderton/Set/Chapter_1.lean +++ b/Bookshelf/Enderton/Set/Chapter_1.lean @@ -1,7 +1,10 @@ -import Mathlib.Init.Set +import Mathlib.Logic.Basic import Mathlib.Data.Set.Basic +import Mathlib.Data.Set.Lattice import Mathlib.Tactic.LibrarySearch +import Common.Set.Basic + /-! # Enderton.Chapter_1 Introduction @@ -104,8 +107,6 @@ theorem exercise_1_2 Show that if `B ⊆ C`, then `𝓟 B ⊆ 𝓟 C`. -/ theorem exercise_1_3 (h : B ⊆ C) : Set.powerset B ⊆ Set.powerset C := by - unfold Set.powerset - simp intro x hx exact Set.Subset.trans hx h @@ -130,4 +131,273 @@ theorem exercise_1_4 (x y : α) (hx : x ∈ B) (hy : y ∈ B) (Set.singleton_subset_iff.mpr hx) (Set.singleton_subset_iff.mpr hy) +/-- ### Exercise 3.1 + +Assume that `A` is the set of integers divisible by `4`. Similarly assume that +`B` and `C` are the sets of integers divisible by `9` and `10`, respectively. +What is in `A ∩ B ∩ C`? +-/ +theorem exercise_3_1 {A B C : Set ℤ} + (hA : A = { x | Dvd.dvd 4 x }) + (hB : B = { x | Dvd.dvd 9 x }) + (hC : C = { x | Dvd.dvd 10 x }) + : ∀ x ∈ (A ∩ B ∩ C), (4 ∣ x) ∧ (9 ∣ x) ∧ (10 ∣ x) := by + intro x h + rw [Set.mem_inter_iff] at h + have ⟨⟨ha, hb⟩, hc⟩ := h + refine ⟨?_, ⟨?_, ?_⟩⟩ + · rw [hA] at ha + exact Set.mem_setOf.mp ha + · rw [hB] at hb + exact Set.mem_setOf.mp hb + · rw [hC] at hc + exact Set.mem_setOf.mp hc + +/-- ### Exercise 3.2 + +Give an example of sets `A` and `B` for which `⋃ A = ⋃ B` but `A ≠ B`. +-/ +theorem exercise_3_2 {A B : Set (Set ℕ)} + (hA : A = {{1}, {2}}) (hB : B = {{1, 2}}) + : Set.sUnion A = Set.sUnion B ∧ A ≠ B := by + apply And.intro + · show ⋃₀ A = ⋃₀ B + ext x + show (∃ t, t ∈ A ∧ x ∈ t) ↔ ∃ t, t ∈ B ∧ x ∈ t + apply Iff.intro + · intro ⟨t, ⟨ht, hx⟩⟩ + rw [hA] at ht + refine ⟨{1, 2}, ⟨by rw [hB]; simp, ?_⟩⟩ + apply Or.elim ht <;> + · intro ht' + rw [ht'] at hx + rw [hx] + simp + · intro ⟨t, ⟨ht, hx⟩⟩ + rw [hB] at ht + rw [ht] at hx + apply Or.elim hx + · intro hx' + exact ⟨{1}, ⟨by rw [hA]; simp, by rw [hx']; simp⟩⟩ + · intro hx' + exact ⟨{2}, ⟨by rw [hA]; simp, by rw [hx']; simp⟩⟩ + · show A ≠ B + -- Find an element that exists in `B` but not in `A`. Extensionality + -- concludes the proof. + intro h + rw [hA, hB, Set.ext_iff] at h + have h₁ := h {1, 2} + simp at h₁ + rw [Set.ext_iff] at h₁ + have h₂ := h₁ 2 + simp at h₂ + +/-- ### Exercise 3.3 + +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 + intro x hx + show ∀ y ∈ x, y ∈ { a | ∃ t, t ∈ A ∧ a ∈ t } + intro y hy + rw [Set.mem_setOf_eq] + exact ⟨x, ⟨hx, hy⟩⟩ + +/-- ### Exercise 3.4 + +Show that if `A ⊆ B`, then `⋃ A ⊆ ⋃ B`. +-/ +theorem exercise_3_4 (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B := by + show ∀ x ∈ { a | ∃ t, t ∈ A ∧ a ∈ t }, x ∈ { a | ∃ t, t ∈ B ∧ a ∈ t } + intro x hx + rw [Set.mem_setOf_eq] at hx + have ⟨t, ⟨ht, hxt⟩⟩ := hx + rw [Set.mem_setOf_eq] + exact ⟨t, ⟨h ht, hxt⟩⟩ + +/-- ### Exercise 3.5 + +Assume that every member of `𝓐` is a subset of `B`. Show that `⋃ 𝓐 ⊆ B`. +-/ +theorem exercise_3_5 (h : ∀ x ∈ 𝓐, x ⊆ B) : ⋃₀ 𝓐 ⊆ B := by + unfold Set.sUnion sSup Set.instSupSetSet + simp only + show ∀ y ∈ { a | ∃ t, t ∈ 𝓐 ∧ a ∈ t }, y ∈ B + intro y hy + rw [Set.mem_setOf_eq] at hy + have ⟨t, ⟨ht𝓐, hyt⟩⟩ := hy + exact (h t ht𝓐) hyt + +/-- ### Exercise 3.6a + +Show that for any set `A`, `⋃ 𝓟 A = A`. +-/ +theorem exercise_3_6a : ⋃₀ (Set.powerset A) = A := by + unfold Set.sUnion sSup Set.instSupSetSet Set.powerset + simp only + ext x + apply Iff.intro + · intro hx + rw [Set.mem_setOf_eq] at hx + have ⟨t, ⟨htl, htr⟩⟩ := hx + rw [Set.mem_setOf_eq] at htl + exact htl htr + · intro hx + rw [Set.mem_setOf_eq] + exact ⟨A, ⟨by rw [Set.mem_setOf_eq], hx⟩⟩ + +/-- ### Exercise 3.6b + +Show that `A ⊆ 𝓟 ⋃ A`. Under what conditions does equality hold? +-/ +theorem exercise_3_6b + : A ⊆ Set.powerset (⋃₀ A) + ∧ (A = Set.powerset (⋃₀ A) ↔ ∃ B, A = Set.powerset B) := by + apply And.intro + · unfold Set.powerset + show ∀ x ∈ A, x ∈ { t | t ⊆ ⋃₀ A } + intro x hx + rw [Set.mem_setOf] + exact exercise_3_3 x hx + · apply Iff.intro + · intro hA + exact ⟨⋃₀ A, hA⟩ + · intro ⟨B, hB⟩ + conv => rhs; rw [hB, exercise_3_6a] + exact hB + +/-- ### Exercise 3.7a + +Show that for any sets `A` and `B`, `𝓟 A ∩ 𝓟 B = 𝓟 (A ∩ B)`. +-/ +theorem exercise_3_7A + : Set.powerset A ∩ Set.powerset B = Set.powerset (A ∩ B) := by + suffices + Set.powerset A ∩ Set.powerset B ⊆ Set.powerset (A ∩ B) ∧ + Set.powerset (A ∩ B) ⊆ Set.powerset A ∩ Set.powerset B from + subset_antisymm this.left this.right + apply And.intro + · unfold Set.powerset + intro x hx + simp only [Set.mem_inter_iff, Set.mem_setOf_eq] at hx + rwa [Set.mem_setOf, Set.subset_inter_iff] + · unfold Set.powerset + simp + intro x hA _ + exact hA + +-- theorem false_of_false_iff_true : (false ↔ true) → false := by simp + +/-- ### Exercise 3.7b (i) + +Show that `𝓟 A ∪ 𝓟 B ⊆ 𝓟 (A ∪ B)`. +-/ +theorem exercise_3_7b_i + : Set.powerset A ∪ Set.powerset B ⊆ Set.powerset (A ∪ B) := by + unfold Set.powerset + intro x hx + simp at hx + apply Or.elim hx + · intro hA + rw [Set.mem_setOf_eq] + exact Set.subset_union_of_subset_left hA B + · intro hB + rw [Set.mem_setOf_eq] + exact Set.subset_union_of_subset_right hB A + +/-- ### Exercise 3.7b (ii) + +Under what conditions does `𝓟 A ∪ 𝓟 B = 𝓟 (A ∪ B)`.? +-/ +theorem exercise_3_7b_ii + : Set.powerset A ∪ Set.powerset B = Set.powerset (A ∪ B) ↔ A ⊆ B ∨ B ⊆ A := by + unfold Set.powerset + apply Iff.intro + · intro h + by_contra nh + rw [not_or] at nh + have ⟨a, hA⟩ := Set.not_subset.mp nh.left + have ⟨b, hB⟩ := Set.not_subset.mp nh.right + rw [Set.ext_iff] at h + have hz := h {a, b} + -- `hz` states that `{a, b} ⊆ A ∨ {a, b} ⊆ B ↔ {a, b} ⊆ A ∪ B`. We show the + -- left-hand side is false but the right-hand side is true, yielding our + -- contradiction. + suffices ¬({a, b} ⊆ A ∨ {a, b} ⊆ B) by + have hz₁ : a ∈ A ∪ B := by + rw [Set.mem_union] + exact Or.inl hA.left + have hz₂ : b ∈ A ∪ B := by + rw [Set.mem_union] + exact Or.inr hB.left + exact absurd (hz.mpr $ Set.mem_mem_imp_pair_subset hz₁ hz₂) this + intro hAB + exact Or.elim hAB + (fun y => absurd (y $ show b ∈ {a, b} by simp) hB.right) + (fun y => absurd (y $ show a ∈ {a, b} by simp) hA.right) + · intro h + ext x + apply Or.elim h + · intro hA + apply Iff.intro + · intro hx + exact Or.elim hx + (Set.subset_union_of_subset_left · B) + (Set.subset_union_of_subset_right · A) + · intro hx + refine Or.inr (Set.Subset.trans hx ?_) + exact subset_of_eq (Set.left_subset_union_eq_self hA) + · intro hB + apply Iff.intro + · intro hx + exact Or.elim hx + (Set.subset_union_of_subset_left · B) + (Set.subset_union_of_subset_right · A) + · intro hx + refine Or.inl (Set.Subset.trans hx ?_) + exact subset_of_eq (Set.right_subset_union_eq_self hB) + +/-- ### Exercise 3.9 + +Give an example of sets `a` and `B` for which `a ∈ B` but `𝓟 a ∉ 𝓟 B`. +-/ +theorem exercise_3_9 (ha : a = {1}) (hB : B = {{1}}) + : a ∈ B ∧ Set.powerset a ∉ Set.powerset B := by + apply And.intro + · rw [ha, hB] + simp + · intro h + have h₁ : Set.powerset a = {∅, {1}} := by + rw [ha] + exact Set.powerset_singleton 1 + have h₂ : Set.powerset B = {∅, {{1}}} := by + rw [hB] + exact Set.powerset_singleton {1} + rw [h₁, h₂] at h + simp at h + apply Or.elim h + · intro h + rw [Set.ext_iff] at h + have := h ∅ + simp at this + · intro h + rw [Set.ext_iff] at h + have := h 1 + simp at this + +/-- ### Exercise 3.10 + +Show that if `a ∈ B`, then `𝓟 a ∈ 𝓟 𝓟 ⋃ B`. +-/ +theorem exercise_3_10 (ha : a ∈ B) + : Set.powerset a ∈ Set.powerset (Set.powerset (⋃₀ B)) := by + have h₁ := exercise_3_3 a ha + have h₂ := exercise_1_3 h₁ + generalize hb : 𝒫 (⋃₀ B) = b + conv => rhs; unfold Set.powerset + rw [← hb, Set.mem_setOf_eq] + exact h₂ + end Enderton.Set.Chapter_1 \ No newline at end of file diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index 71d013f..dd37419 100644 --- a/Common/Set/Basic.lean +++ b/Common/Set/Basic.lean @@ -7,15 +7,17 @@ Additional theorems and definitions useful in the context of `Set`s. namespace Set +/-! ## Minkowski Sum -/ + /- -The Minkowski sum of two sets `s` and `t` is the set +The Minkowski sum of two `Set`s `s` and `t` is the set `s + t = { a + b : a ∈ s, b ∈ t }`. -/ def minkowskiSum {α : Type u} [Add α] (s t : Set α) := { x | ∃ a ∈ s, ∃ b ∈ t, x = a + b } /-- -The sum of two sets is nonempty **iff** the summands are nonempty. +The sum of two `Set`s is nonempty **iff** the summands are nonempty. -/ theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α] {s t : Set α} @@ -30,12 +32,59 @@ theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α] · intro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ exact ⟨a + b, ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩⟩ +/-! ## Characteristic Function -/ + /-- -The characteristic function of a set `S`. +The characteristic function of a `Set` `S`. It returns `1` if the specified input belongs to `S` and `0` otherwise. -/ def characteristic (S : Set α) (x : α) [Decidable (x ∈ S)] : Nat := if x ∈ S then 1 else 0 +/-! ## Subsets -/ + +/-- +Every `Set` is a subset of itself. +-/ +theorem subset_self (S : Set α) : S ⊆ S := by + intro _ hs + exact hs + +/-- +If `Set` `A` is a subset of `Set` `B`, then `A ∪ B = B`. +-/ +theorem left_subset_union_eq_self {A B : Set α} (h : A ⊆ B) + : A ∪ B = B := by + rw [Set.ext_iff] + intro x + apply Iff.intro + · intro hU + apply Or.elim hU + · intro hA + exact h hA + · simp + · intro hB + exact Or.inr hB + +/-- +If `Set` `B` is a subset of `Set` `A`, then `A ∪ B = B`. +-/ +theorem right_subset_union_eq_self {A B : Set α} (h : B ⊆ A) + : A ∪ B = A := by + rw [Set.union_comm] + exact left_subset_union_eq_self h + +/-- +If `x` and `y` are members of `Set` `A`, it follows `{x, y}` is a subset of `A`. +-/ +theorem mem_mem_imp_pair_subset {x y : α} + (hx : x ∈ A) (hy : y ∈ A) : ({x, y} : Set α) ⊆ A := by + intro a ha + apply Or.elim ha + · intro hx' + rwa [hx'] + · intro hy' + rwa [hy'] + end Set \ No newline at end of file diff --git a/preamble.tex b/preamble.tex index 368cd8e..abdfb77 100644 --- a/preamble.tex +++ b/preamble.tex @@ -29,7 +29,7 @@ \newcommand\@linespace{\vspace{10pt}} \newcommand\linedivider{\@linespace\hrule\@linespace} \WithSuffix\newcommand\linedivider*{\@linespace\hrule} -\newcommand\suitdivider{$$\spadesuit\spadesuit\spadesuit$$} +\newcommand\suitdivider{$$\spadesuit\;\spadesuit\;\spadesuit$$} % ======================================== % Linking @@ -89,6 +89,7 @@ \newcommand\@statement[1]{% \linedivider*\paragraph{\normalfont\normalsize\textit{#1.}}} +\newenvironment{answer}{\@statement{Answer}}{\hfill$\square$} \newenvironment{axiom}{\@statement{Axiom}}{\hfill$\square$} \newenvironment{definition}{\@statement{Definition}}{\hfill$\square$} \renewenvironment{proof}{\@statement{Proof}}{\hfill$\square$} @@ -131,7 +132,7 @@ \newcommand{\ico}[2]{\left[#1, #2\right)} \newcommand{\ioc}[2]{\left(#1, #2\right]} \newcommand{\ioo}[2]{\left(#1, #2\right)} -\newcommand{\powerset}[1]{\mathscr{P}\,#1} +\newcommand{\powerset}[1]{\mathscr{P}#1} \newcommand{\ubar}[1]{\text{\b{$#1$}}} \let\oldemptyset\emptyset