r
/
bookshelf
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Enderton "Algebra of Sets" identities and create `Chapter_2.lean`.

finite-set-exercises
Joshua Potter 2023-05-23 09:18:23 -06:00
parent 6deeb57409
commit fd816a97bc
4 changed files with 528 additions and 320 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Bookshelf/Enderton/Set.lean
View File

@ -1 +1,2 @@
import Bookshelf.Enderton.Set.Chapter_1 import Bookshelf.Enderton.Set.Chapter_1
import Bookshelf.Enderton.Set.Chapter_2

287
Bookshelf/Enderton/Set.tex
View File

@ -510,8 +510,8 @@ What is in $A \cap B \cap C$?
\begin{answer} \begin{answer}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_1} {Enderton.Set.Chapter\_2.exercise\_3\_1}
The set of integers divisible by $4$, $9$, and $10$. 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} \begin{answer}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_2} {Enderton.Set.Chapter\_2.exercise\_3\_2}
Let $A = \{\{1\}, \{2\}\}$ and $B = \{\{1, 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} \begin{proof}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_3} {Enderton.Set.Chapter\_2.exercise\_3\_3}
Let $x \in A$. Let $x \in A$.
By definition, $$\bigcup A = \{ y \mid (\exists b \in A) y \in b\}.$$ 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} \begin{proof}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_4} {Enderton.Set.Chapter\_2.exercise\_3\_4}
Let $A$ and $B$ be sets such that $A \subseteq B$. Let $A$ and $B$ be sets such that $A \subseteq B$.
Let $x \in \bigcup A$. Let $x \in \bigcup A$.
@ -579,8 +579,8 @@ Show that $\bigcup \mathscr{A} \subseteq B$.
\begin{proof} \begin{proof}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_5} {Enderton.Set.Chapter\_2.exercise\_3\_5}
Let $x \in \bigcup \mathscr{A}$. Let $x \in \bigcup \mathscr{A}$.
By definition, By definition,
@ -600,8 +600,8 @@ Show that for any set $A$, $\bigcup \powerset{A} = A$.
\begin{proof} \begin{proof}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_6a} {Enderton.Set.Chapter\_2.exercise\_3\_6a}
We prove that (i) $\bigcup \powerset{A} \subseteq A$ and (ii) We prove that (i) $\bigcup \powerset{A} \subseteq A$ and (ii)
$A \subseteq \bigcup \powerset{A}$. $A \subseteq \bigcup \powerset{A}$.
@ -641,8 +641,8 @@ Under what conditions does equality hold?
\begin{proof} \begin{proof}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_6b} {Enderton.Set.Chapter\_2.exercise\_3\_6b}
Let $x \in A$. Let $x \in A$.
By \nameref{sub:exercise-3.3}, $x$ is a subset of $\bigcup 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} \begin{proof}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_7a} {Enderton.Set.Chapter\_2.exercise\_3\_7a}
Let $A$ and $B$ be arbitrary sets. We show that Let $A$ and $B$ be arbitrary sets. We show that
$\powerset{A} \cap \powerset{B} \subseteq \powerset{(A \cap B)}$ and then $\powerset{A} \cap \powerset{B} \subseteq \powerset{(A \cap B)}$ and then
@ -741,11 +741,11 @@ Under what conditions does equality hold?
\statementpadding \statementpadding
\lean*{Bookshelf/Enderton/Set/Chapter\_1} \lean*{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_7b\_i} {Enderton.Set.Chapter\_2.exercise\_3\_7b\_i}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_7b\_ii} {Enderton.Set.Chapter\_2.exercise\_3\_7b\_ii}
Let $x \in \powerset{A} \cup \powerset{B}$. Let $x \in \powerset{A} \cup \powerset{B}$.
By definition, $x \in \powerset{A}$ or $x \in \powerset{B}$ (or both). 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} \begin{answer}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_9} {Enderton.Set.Chapter\_2.exercise\_3\_9}
Let $a = \{1\}$ and $B = \{\{1\}\}$. Let $a = \{1\}$ and $B = \{\{1\}\}$.
Then Then
@ -858,8 +858,8 @@ Show that if $a \in B$, then $\powerset{a} \in \powerset{\powerset{\bigcup B}}$.
\begin{proof} \begin{proof}
\lean{Bookshelf/Enderton/Set/Chapter\_1} \lean{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_1.exercise\_3\_10} {Enderton.Set.Chapter\_2.exercise\_3\_10}
Suppose $a \in B$. Suppose $a \in B$.
By \nameref{sub:exercise-3.3}, $a \subseteq \bigcup 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} \lean{Mathlib/Data/Set/Basic}{Set.inter\_comm}
Let $A$ and $B$ be sets. \noindent Let $A$ and $B$ be sets.
We show (i) $A \cup B = B \cup A$ and then (ii) $A \cap B = B \cap A$. We prove that
\begin{enumerate}[(i)]
\item $A \cup B = B \cup A$
\item $A \cap B = B \cap A$.
\end{enumerate}
\paragraph{(i)}% \paragraph{(i)}%
@ -933,9 +937,12 @@ For any sets $A$, $B$ and $C$,
\lean{Mathlib/Data/Set/Basic}{Set.inter\_assoc} \lean{Mathlib/Data/Set/Basic}{Set.inter\_assoc}
Let $A$, $B$, and $C$ be sets. \noindent Let $A$, $B$, and $C$ be sets.
We show (i) $A \cup (B \cup C) = (A \cup B) \cup C$ and then (ii) We prove that
$A \cap (B \cap C) = (A \cap B) \cap C$. \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)}% \paragraph{(i)}%
@ -987,9 +994,12 @@ For any sets $A$, $B$, and $C$,
\lean{Mathlib/Data/Set/Basic}{Set.union\_distrib\_left} \lean{Mathlib/Data/Set/Basic}{Set.union\_distrib\_left}
Let $A$, $B$, and $C$ be sets. \noindent 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) We prove that
$A \cup (B \cap C) = (A \cup B) \cap (A \cup C)$. \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)}% \paragraph{(i)}%
@ -1040,9 +1050,12 @@ For any sets $A$, $B$, and $C$,
\lean{Mathlib/Data/Set/Basic}{Set.diff\_inter} \lean{Mathlib/Data/Set/Basic}{Set.diff\_inter}
Let $A$, $B$, and $C$ be sets. \noindent Let $A$, $B$, and $C$ be sets.
We show (i) $C - (A \cup B) = (C - A) \cap (C - B)$ and then (ii) We prove that
$C - (A \cap B) = (C - A) \cup (C - B)$. \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)}% \paragraph{(i)}%
@ -1099,8 +1112,13 @@ For any set $A$,
\lean{Mathlib/Data/Set/Basic}{Set.inter\_diff\_self} \lean{Mathlib/Data/Set/Basic}{Set.inter\_diff\_self}
Let $A$ be an arbitrary set. We prove (i) that $A \cup \emptyset = A$, (ii) \noindent Let $A$ be an arbitrary set.
$A \cap \emptyset = \emptyset$, and (iii) $A \cap (C - A) = \emptyset$. 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)}% \paragraph{(i)}%
@ -1143,7 +1161,7 @@ For any set $A$,
\end{proof} \end{proof}
\subsection{\unverified{Monotonicity}}% \subsection{\verified{Monotonicity}}%
\label{sub:monotonicity} \label{sub:monotonicity}
For any sets $A$, $B$, and $C$, For any sets $A$, $B$, and $C$,
@ -1155,11 +1173,68 @@ For any sets $A$, $B$, and $C$,
\begin{proof} \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} \end{proof}
\subsection{\unverified{Anti-monotonicity}}% \subsection{\verified{Anti-monotonicity}}%
\label{sub:anti-monotonicity} \label{sub:anti-monotonicity}
For any sets $A$, $B$, and $C$, For any sets $A$, $B$, and $C$,
@ -1170,11 +1245,46 @@ For any sets $A$, $B$, and $C$,
\begin{proof} \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} \end{proof}
\subsection{\unverified{General Distributive Laws}}% \subsection{\partial{General Distributive Laws}}%
\label{sub:general-distributive-laws} \label{sub:general-distributive-laws}
For any sets $A$ and $\mathscr{B}$, For any sets $A$ and $\mathscr{B}$,
@ -1188,11 +1298,53 @@ For any sets $A$ and $\mathscr{B}$,
\begin{proof} \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} \end{proof}
\subsection{\unverified{General De Morgan's Laws}}% \subsection{\partial{General De Morgan's Laws}}%
\label{sub:general-de-morgans-laws} \label{sub:general-de-morgans-laws}
For any set $C$ and $\mathscr{A} \neq \emptyset$, For any set $C$ and $\mathscr{A} \neq \emptyset$,
@ -1203,7 +1355,52 @@ For any set $C$ and $\mathscr{A} \neq \emptyset$,
\begin{proof} \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} \end{proof}

274
Bookshelf/Enderton/Set/Chapter_1.lean
View File

@ -1,9 +1,4 @@
import Mathlib.Logic.Basic
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Tactic.LibrarySearch
import Common.Set.Basic
/-! # Enderton.Chapter_1 /-! # 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 hx)
(Set.singleton_subset_iff.mpr hy) (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 end Enderton.Set.Chapter_1

284
Bookshelf/Enderton/Set/Chapter_2.lean Normal file
View File

@ -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