From fd816a97bcfca4d8134f57d7417acbd84df721a5 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 23 May 2023 09:18:23 -0600 Subject: [PATCH] Enderton "Algebra of Sets" identities and create `Chapter_2.lean`. --- Bookshelf/Enderton/Set.lean | 3 +- Bookshelf/Enderton/Set.tex | 287 ++++++++++++++++++++++---- Bookshelf/Enderton/Set/Chapter_1.lean | 274 ------------------------ Bookshelf/Enderton/Set/Chapter_2.lean | 284 +++++++++++++++++++++++++ 4 files changed, 528 insertions(+), 320 deletions(-) create mode 100644 Bookshelf/Enderton/Set/Chapter_2.lean diff --git a/Bookshelf/Enderton/Set.lean b/Bookshelf/Enderton/Set.lean index 81598b8..52a12d4 100644 --- a/Bookshelf/Enderton/Set.lean +++ b/Bookshelf/Enderton/Set.lean @@ -1 +1,2 @@ -import Bookshelf.Enderton.Set.Chapter_1 \ No newline at end of file +import Bookshelf.Enderton.Set.Chapter_1 +import Bookshelf.Enderton.Set.Chapter_2 \ No newline at end of file diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index b34b667..907bf4d 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -510,8 +510,8 @@ What is in $A \cap B \cap C$? \begin{answer} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_1} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_3\_1} The set of integers divisible by $4$, $9$, and $10$. @@ -525,8 +525,8 @@ Give an example of sets $A$ and $B$ for which $\bigcup A = \bigcup B$ but \begin{answer} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_2} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_3\_2} Let $A = \{\{1\}, \{2\}\}$ and $B = \{\{1, 2\}\}$. @@ -540,8 +540,8 @@ Show that every member of a set $A$ is a subset of $\bigcup A$. \begin{proof} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_3} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_3\_3} Let $x \in A$. By definition, $$\bigcup A = \{ y \mid (\exists b \in A) y \in b\}.$$ @@ -558,8 +558,8 @@ Show that if $A \subseteq B$, then $\bigcup A \subseteq \bigcup B$. \begin{proof} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_4} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_3\_4} Let $A$ and $B$ be sets such that $A \subseteq B$. Let $x \in \bigcup A$. @@ -579,8 +579,8 @@ Show that $\bigcup \mathscr{A} \subseteq B$. \begin{proof} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_5} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_3\_5} Let $x \in \bigcup \mathscr{A}$. By definition, @@ -600,8 +600,8 @@ Show that for any set $A$, $\bigcup \powerset{A} = A$. \begin{proof} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_6a} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_3\_6a} We prove that (i) $\bigcup \powerset{A} \subseteq A$ and (ii) $A \subseteq \bigcup \powerset{A}$. @@ -641,8 +641,8 @@ Under what conditions does equality hold? \begin{proof} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_6b} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_3\_6b} Let $x \in A$. By \nameref{sub:exercise-3.3}, $x$ is a subset of $\bigcup A$. @@ -690,8 +690,8 @@ Show that for any sets $A$ and $B$, \begin{proof} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_7a} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.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 @@ -741,11 +741,11 @@ Under what conditions does equality hold? \statementpadding - \lean*{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_7b\_i} + \lean*{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_3\_7b\_i} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_7b\_ii} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.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). @@ -837,8 +837,8 @@ Give an example of sets $a$ and $B$ for which $a \in B$ but \begin{answer} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_9} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_3\_9} Let $a = \{1\}$ and $B = \{\{1\}\}$. Then @@ -858,8 +858,8 @@ Show that if $a \in B$, then $\powerset{a} \in \powerset{\powerset{\bigcup B}}$. \begin{proof} - \lean{Bookshelf/Enderton/Set/Chapter\_1} - {Enderton.Set.Chapter\_1.exercise\_3\_10} + \lean{Bookshelf/Enderton/Set/Chapter\_2} + {Enderton.Set.Chapter\_2.exercise\_3\_10} Suppose $a \in B$. By \nameref{sub:exercise-3.3}, $a \subseteq \bigcup B$. @@ -891,8 +891,12 @@ For any sets $A$ and $B$, \lean{Mathlib/Data/Set/Basic}{Set.inter\_comm} - Let $A$ and $B$ be sets. - We show (i) $A \cup B = B \cup A$ and then (ii) $A \cap B = B \cap A$. + \noindent Let $A$ and $B$ be sets. + We prove that + \begin{enumerate}[(i)] + \item $A \cup B = B \cup A$ + \item $A \cap B = B \cap A$. + \end{enumerate} \paragraph{(i)}% @@ -933,9 +937,12 @@ For any sets $A$, $B$ and $C$, \lean{Mathlib/Data/Set/Basic}{Set.inter\_assoc} - Let $A$, $B$, and $C$ be sets. - We show (i) $A \cup (B \cup C) = (A \cup B) \cup C$ and then (ii) - $A \cap (B \cap C) = (A \cap B) \cap C$. + \noindent Let $A$, $B$, and $C$ be sets. + We prove that + \begin{enumerate}[(i)] + \item $A \cup (B \cup C) = (A \cup B) \cup C$ + \item $A \cap (B \cap C) = (A \cap B) \cap C$ + \end{enumerate} \paragraph{(i)}% @@ -987,9 +994,12 @@ For any sets $A$, $B$, and $C$, \lean{Mathlib/Data/Set/Basic}{Set.union\_distrib\_left} - Let $A$, $B$, and $C$ be sets. - We show (i) $A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$ and then (ii) - $A \cup (B \cap C) = (A \cup B) \cap (A \cup C)$. + \noindent Let $A$, $B$, and $C$ be sets. + We prove that + \begin{enumerate}[(i)] + \item $A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$ + \item $A \cup (B \cap C) = (A \cup B) \cap (A \cup C)$ + \end{enumerate} \paragraph{(i)}% @@ -1040,9 +1050,12 @@ For any sets $A$, $B$, and $C$, \lean{Mathlib/Data/Set/Basic}{Set.diff\_inter} - Let $A$, $B$, and $C$ be sets. - We show (i) $C - (A \cup B) = (C - A) \cap (C - B)$ and then (ii) - $C - (A \cap B) = (C - A) \cup (C - B)$. + \noindent Let $A$, $B$, and $C$ be sets. + We prove that + \begin{enumerate}[(i)] + \item $C - (A \cup B) = (C - A) \cap (C - B)$ + \item $C - (A \cap B) = (C - A) \cup (C - B)$ + \end{enumerate} \paragraph{(i)}% @@ -1099,8 +1112,13 @@ For any set $A$, \lean{Mathlib/Data/Set/Basic}{Set.inter\_diff\_self} - Let $A$ be an arbitrary set. We prove (i) that $A \cup \emptyset = A$, (ii) - $A \cap \emptyset = \emptyset$, and (iii) $A \cap (C - A) = \emptyset$. + \noindent Let $A$ be an arbitrary set. + We prove that + \begin{enumerate}[(i)] + \item $A \cup \emptyset = A$ + \item $A \cap \emptyset = \emptyset$ + \item $A \cap (C - A) = \emptyset$ + \end{enumerate} \paragraph{(i)}% @@ -1143,7 +1161,7 @@ For any set $A$, \end{proof} -\subsection{\unverified{Monotonicity}}% +\subsection{\verified{Monotonicity}}% \label{sub:monotonicity} For any sets $A$, $B$, and $C$, @@ -1155,11 +1173,68 @@ For any sets $A$, $B$, and $C$, \begin{proof} - TODO + \statementpadding + + \lean*{Mathlib/Data/Set/Basic}{Set.union\_subset\_union\_left} + + \lean*{Mathlib/Data/Set/Basic}{Set.inter\_subset\_inter\_left} + + \lean{Mathlib/Data/Set/Lattice}{Set.sUnion\_mono} + + \noindent Let $A$, $B$, and $C$ be arbitrary sets. + We prove that + \begin{enumerate}[(i)] + \item $A \subseteq B \Rightarrow A \cup C \subseteq B \cup C$ + \item $A \subseteq B \Rightarrow A \cap C \subseteq B \cap C$ + \item $A \subseteq B \Rightarrow \bigcup A \subseteq \bigcup B$ + \end{enumerate} + + \paragraph{(i)}% + + Suppose $A \subseteq B$. + Let $x \in A \cup C$. + There are two cases to consider. + + \subparagraph{Case 1}% + + Suppose $x \in A$. + Then, by definition of the subset, $x \in B$. + Therefore $x \in B \cup C$. + + \subparagraph{Case 2}% + + Suppose $x \in C$. + Then $x$ is trivially a member of $B \cup C$. + + \subparagraph{Conclusion}% + + Since these cases are exhaustive and both imply $x \in B \cup C$, it + follows $A \cup C \subseteq B \cup C$. + + \paragraph{(ii)}% + + Suppose $A \subseteq B$. + Let $x \in A \cap C$. + Then, by definition of the intersection of sets, $x \in A$ and $x \in C$. + By definition of the subset, $x \in A$ implies $x \in B$. + Therefore $x \in B$ and $x \in C$. + That is, $x \in B \cap C$. + Since this holds for arbitrary $x \in A \cap C$, it follows + $A \cap C \subseteq B \cap C$. + + \paragraph{(iii)}% + + Suppose $A \subseteq B$. + Let $x \in \bigcup A$. + Then, by definition of the union of sets, there exists some $b \in A$ such + that $x \in b$. + By definition of the subset, $b \in B$ as well. + Another application of the definition of the union of sets immediately + implies that $x$ is a member of $\bigcup B$. \end{proof} -\subsection{\unverified{Anti-monotonicity}}% +\subsection{\verified{Anti-monotonicity}}% \label{sub:anti-monotonicity} For any sets $A$, $B$, and $C$, @@ -1170,11 +1245,46 @@ For any sets $A$, $B$, and $C$, \begin{proof} - TODO + \statementpadding + + \lean*{Mathlib/Data/Set/Basic}{Set.diff\_subset\_diff\_right} + + \lean{Mathlib/Data/Set/Lattice}{Set.sInter\_subset\_sInter} + + \noindent Let $A$, $B$, and $C$ be arbitrary sets. + We prove that + \begin{enumerate}[(i)] + \item $A \subseteq B \Rightarrow C - B \subseteq C - A$ + \item $\emptyset \neq A \subseteq B \Rightarrow + \bigcap B \subseteq \bigcap A$ + \end{enumerate} + + \paragraph{(i)}% + + Suppose $A \subseteq B$. + Let $x \in C - B$. + By definition of the relative complement, $x \in C$ and $x \not\in B$. + Then $x$ cannot be a member of $A$, since otherwise this would contradict + our subset hypothesis. + That is, $x \in C$ and $x \not\in A$. + Therefore $x \in C - A$. + Since this holds for arbitrary $x \in C - B$, it follows that + $C - B \subseteq C - A$. + + \paragraph{(ii)}% + + Suppose $A \neq \emptyset$ and $A \subseteq B$. + Then $B \neq \emptyset$. + Let $x \in \bigcap B$. + By definition of the intersection of sets, for all $b \in B$, $x \in b$. + But then, by definition of the subset, for all $a \in A$, $x \in a$. + Therefore $x \in \bigcap A$. + Since this holds for arbitrary $x \in \bigcap B$, it follows that + $\bigcap B \subseteq \bigcap A$. \end{proof} -\subsection{\unverified{General Distributive Laws}}% +\subsection{\partial{General Distributive Laws}}% \label{sub:general-distributive-laws} For any sets $A$ and $\mathscr{B}$, @@ -1188,11 +1298,53 @@ For any sets $A$ and $\mathscr{B}$, \begin{proof} - TODO + Let $A$ and $\mathscr{B}$ be sets. + We prove that + \begin{enumerate}[(i)] + \item For $\mathscr{B} \neq \emptyset$, + $A \cup \bigcap \mathscr{B} = + \bigcap\; \{ A \cup X \mid X \in \mathscr{B} \}$. + \item $A \cap \bigcup \mathscr{B} = + \bigcup\; \{ A \cap X \mid X \in \mathscr{B} \}$ + \end{enumerate} + + \paragraph{(i)}% + + Suppose $\mathscr{B}$ is nonempty. + Then $\bigcap \mathscr{B}$ is defined. + By definition of the union and intersection of sets, + \begin{align*} + A \cup \bigcap \mathscr{B} + & = \{ x \mid x \in A \lor x \in \bigcap \mathscr{B} \} \\ + & = \{ x \mid x \in A \lor + x \in \{ y \mid (\forall b \in \mathscr{B}), y \in b \}\} \\ + & = \{ x \mid x \in A \lor (\forall b \in \mathscr{B}), x \in b \} \\ + & = \{ x \mid \forall b \in \mathscr{B}, x \in A \lor x \in b \} \\ + & = \{ x \mid \forall b \in \mathscr{B}, x \in A \cup b \} \\ + & = \{ x \mid + x \in \bigcap\; \{ A \cup X \mid X \in \mathscr{B} \}\} \\ + & = \bigcap\; \{ A \cup X \mid X \in \mathscr{B} \}. + \end{align*} + + \paragraph{(ii)}% + + By definition of the intersection and union of sets, + \begin{align*} + A \cap \bigcup \mathscr{B} + & = \{ x \mid x \in A \land x \in \bigcup \mathscr{B} \} \\ + & = \{ x \mid x \in A \land + x \in \{ y \mid (\exists b \in \mathscr{B}), y \in b \}\} \\ + & = \{ x \mid x \in A \land (\exists b \in \mathscr{B}), x \in b \} \\ + & = \{ x \mid \exists b \in \mathscr{B}, x \in A \land x \in b \} \\ + & = \{ x \mid \exists b \in \mathscr{B} x \in A \cap b \} \\ + & = \{ x \mid + x \in \bigcup\; \{ A \cap X \mid X \in \mathscr{B} \}\} \\ + & = \bigcup\; \{ A \cap X \mid X \in \mathscr{B} \}. + \end{align*} \end{proof} -\subsection{\unverified{General De Morgan's Laws}}% +\subsection{\partial{General De Morgan's Laws}}% \label{sub:general-de-morgans-laws} For any set $C$ and $\mathscr{A} \neq \emptyset$, @@ -1203,7 +1355,52 @@ For any set $C$ and $\mathscr{A} \neq \emptyset$, \begin{proof} - TODO + Let $C$ and $\mathscr{A}$ be sets such that $\mathscr{A} \neq \emptyset$. + We prove that + \begin{enumerate}[(i)] + \item $C - \bigcup \mathscr{A} = + \bigcap\; \{ C - X \mid X \in \mathscr{A} \}$ + \item $C - \bigcap \mathscr{A} = + \bigcup\; \{ C - X \mid X \in \mathscr{A} \}$ + \end{enumerate} + + \paragraph{(i)}% + + By definition of the relative complement, union, and intersection of sets, + \begin{align*} + C - \bigcup \mathscr{A} + & = \{ x \mid x \in C \land x \not\in \bigcup \mathscr{A} \} \\ + & = \{ x \mid x \in C \land + x \not\in \{ y \mid (\exists b \in \mathscr{A}) y \in b \}\} \\ + & = \{ x \mid x \in C \land + \neg(\exists b \in \mathscr{A}, x \in b) \} \\ + & = \{ x \mid x \in C \land + (\forall b \in \mathscr{A}, x \not\in b) \} \\ + & = \{ x \mid + \forall b \in \mathscr{A}, x \in C \land x \not\in b \} \\ + & = \{ x \mid \forall b \in \mathscr{A}, x \in C - b \} \\ + & = \{ x \mid x \in \bigcap\; \{ C - X \mid X \in \mathscr{A} \} \\ + & = \bigcap\; \{ C - X \mid X \in \mathscr{A} \}. + \end{align*} + + \paragraph{(ii)}% + + By definition of the relative complement, union, and intersection of sets, + \begin{align*} + C - \bigcap \mathscr{A} + & = \{ x \mid x \in C \land x \not\in \bigcap \mathscr{A} \} \\ + & = \{ x \mid x \in C \land + x \not\in \{ y \mid (\forall b \in \mathscr{A}) y \in b \}\} \\ + & = \{ x \mid x \in C \land + \neg(\forall b \in \mathscr{A}, x \in b) \} \\ + & = \{ x \mid x \in C \land + \exists b \in \mathscr{A}, x \not\in b \} \\ + & = \{ x \mid + \exists b \in \mathscr{A}, x \in C \land x \not\in b \} \\ + & = \{ x \mid \exists b \in \mathscr{A}, x \in C - b \} \\ + & = \{ x \mid x \in \bigcup\; \{ C - X \mid X \in \mathscr{A} \} \} \\ + & = \bigcup\; \{ C - X \mid X \in \mathscr{A} \}. + \end{align*} \end{proof} diff --git a/Bookshelf/Enderton/Set/Chapter_1.lean b/Bookshelf/Enderton/Set/Chapter_1.lean index 996ac5c..e586f4e 100644 --- a/Bookshelf/Enderton/Set/Chapter_1.lean +++ b/Bookshelf/Enderton/Set/Chapter_1.lean @@ -1,9 +1,4 @@ -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 @@ -131,273 +126,4 @@ 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/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean new file mode 100644 index 0000000..f7f336f --- /dev/null +++ b/Bookshelf/Enderton/Set/Chapter_2.lean @@ -0,0 +1,284 @@ +import Mathlib.Data.Set.Basic +import Mathlib.Data.Set.Lattice + +import Bookshelf.Enderton.Set.Chapter_1 +import Common.Set.Basic + +/-! # Enderton.Chapter_2 + +Axioms and Operations +-/ + +namespace Enderton.Set.Chapter_2 + + +/-- ### 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₂ := Chapter_1.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_2 \ No newline at end of file