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

Enderton, basic axioms/unions exercises.

finite-set-exercises
Joshua Potter 2023-05-21 18:32:59 -06:00
parent 66df65c14b
commit 8279131d74
4 changed files with 586 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

291
Bookshelf/Enderton/Set.tex
View File

@ -432,7 +432,7 @@ List all the members of $V_4$.
\section{Exercises 3}% \section{Exercises 3}%
\label{sec:exercises-3} \label{sec:exercises-3}
\subsection{\unverified{Exercise 3.1}}% \subsection{\verified{Exercise 3.1}}%
\label{sub:exercise-3.1} \label{sub:exercise-3.1}
Assume that $A$ is the set of integers divisible by $4$. 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. $10$, respectively.
What is in $A \cap B \cap C$? 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} \label{sub:exercise-3.2}
Give an example of sets $A$ and $B$ for which $\bigcup A = \bigcup B$ but Give an example of sets $A$ and $B$ for which $\bigcup A = \bigcup B$ but
$A \neq B$. $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} \label{sub:exercise-3.3}
Show that every member of a set $A$ is a subset of $\bigcup A$. 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} \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} \end{proof}
\subsection{\unverified{Exercise 3.4}}% \subsection{\verified{Exercise 3.4}}%
\label{sub:exercise-3.4} \label{sub:exercise-3.4}
Show that if $A \subseteq B$, then $\bigcup A \subseteq \bigcup B$. Show that if $A \subseteq B$, then $\bigcup A \subseteq \bigcup B$.
\begin{proof} \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} \end{proof}
\subsection{\unverified{Exercise 3.5}}% \subsection{\verified{Exercise 3.5}}%
\label{sub:exercise-3.5} \label{sub:exercise-3.5}
Assume that every member of $\mathscr{A}$ is a subset of $B$. 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} \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} \end{proof}
\subsection{\unverified{Exercise 3.6a}}% \subsection{\verified{Exercise 3.6a}}%
\label{sub:exercise-3.6a} \label{sub:exercise-3.6a}
Show that for any set $A$, $\bigcup \powerset{A} = A$. Show that for any set $A$, $\bigcup \powerset{A} = A$.
\begin{proof} \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} \end{proof}
\subsection{\unverified{Exercise 3.6b}}% \subsection{\verified{Exercise 3.6b}}%
\label{sub:exercise-3.6b} \label{sub:exercise-3.6b}
Show that $A \subseteq \powerset{\bigcup A}$. Show that $A \subseteq \powerset{\bigcup A}$.
@ -512,35 +573,176 @@ Under what conditions does equality hold?
\begin{proof} \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} \end{proof}
\subsection{\unverified{Exercise 3.7a}}% \subsection{\verified{Exercise 3.7a}}%
\label{sub:exercise-3.7a} \label{sub:exercise-3.7a}
Show that for any sets $A$ and $B$, 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} \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} \end{proof}
\subsection{\unverified{Exercise 3.7b}}% \subsection{\verified{Exercise 3.7b}}%
\label{sub: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? Under what conditions does equality hold?
\begin{proof} \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} \end{proof}
\subsection{\unverified{Exercise 3.8}}% \subsection{\partial{Exercise 3.8}}%
\label{sub:exercise-3.8} \label{sub:exercise-3.8}
Show that there is no set to which every singleton (that is, every set of the 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} \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} \end{proof}
\subsection{\unverified{Exercise 3.9}}% \subsection{\verified{Exercise 3.9}}%
\label{sub:exercise-3.9} \label{sub:exercise-3.9}
Give an example of sets $a$ and $B$ for which $a \in B$ but 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} \label{sub:exercise-3.10}
Show that if $a \in B$, then $\powerset{a} \in \powerset{\powerset{\bigcup B}}$. 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} \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} \end{proof}

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

@ -1,7 +1,10 @@
import Mathlib.Init.Set import Mathlib.Logic.Basic
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Tactic.LibrarySearch import Mathlib.Tactic.LibrarySearch
import Common.Set.Basic
/-! # Enderton.Chapter_1 /-! # Enderton.Chapter_1
Introduction Introduction
@ -104,8 +107,6 @@ theorem exercise_1_2
Show that if `B ⊆ C`, then `𝓟 B ⊆ 𝓟 C`. Show that if `B ⊆ C`, then `𝓟 B ⊆ 𝓟 C`.
-/ -/
theorem exercise_1_3 (h : B ⊆ C) : Set.powerset B ⊆ Set.powerset C := by theorem exercise_1_3 (h : B ⊆ C) : Set.powerset B ⊆ Set.powerset C := by
unfold Set.powerset
simp
intro x hx intro x hx
exact Set.Subset.trans hx h 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 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

55
Common/Set/Basic.lean
View File

@ -7,15 +7,17 @@ Additional theorems and definitions useful in the context of `Set`s.
namespace Set 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 }`. `s + t = { a + b : a ∈ s, b ∈ t }`.
-/ -/
def minkowskiSum {α : Type u} [Add α] (s t : Set α) := def minkowskiSum {α : Type u} [Add α] (s t : Set α) :=
{ x | ∃ a ∈ s, ∃ b ∈ t, x = a + b } { 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 α] theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α]
{s t : Set α} {s t : Set α}
@ -30,12 +32,59 @@ theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α]
· intro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ · intro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩
exact ⟨a + b, ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩⟩ 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. It returns `1` if the specified input belongs to `S` and `0` otherwise.
-/ -/
def characteristic (S : Set α) (x : α) [Decidable (x ∈ S)] : Nat := def characteristic (S : Set α) (x : α) [Decidable (x ∈ S)] : Nat :=
if x ∈ S then 1 else 0 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 end Set

5
preamble.tex
View File

@ -29,7 +29,7 @@
\newcommand\@linespace{\vspace{10pt}} \newcommand\@linespace{\vspace{10pt}}
\newcommand\linedivider{\@linespace\hrule\@linespace} \newcommand\linedivider{\@linespace\hrule\@linespace}
\WithSuffix\newcommand\linedivider*{\@linespace\hrule} \WithSuffix\newcommand\linedivider*{\@linespace\hrule}
\newcommand\suitdivider{$$\spadesuit\spadesuit\spadesuit$$} \newcommand\suitdivider{$$\spadesuit\;\spadesuit\;\spadesuit$$}
% ======================================== % ========================================
% Linking % Linking
@ -89,6 +89,7 @@
\newcommand\@statement[1]{% \newcommand\@statement[1]{%
\linedivider*\paragraph{\normalfont\normalsize\textit{#1.}}} \linedivider*\paragraph{\normalfont\normalsize\textit{#1.}}}
\newenvironment{answer}{\@statement{Answer}}{\hfill$\square$}
\newenvironment{axiom}{\@statement{Axiom}}{\hfill$\square$} \newenvironment{axiom}{\@statement{Axiom}}{\hfill$\square$}
\newenvironment{definition}{\@statement{Definition}}{\hfill$\square$} \newenvironment{definition}{\@statement{Definition}}{\hfill$\square$}
\renewenvironment{proof}{\@statement{Proof}}{\hfill$\square$} \renewenvironment{proof}{\@statement{Proof}}{\hfill$\square$}
@ -131,7 +132,7 @@
\newcommand{\ico}[2]{\left[#1, #2\right)} \newcommand{\ico}[2]{\left[#1, #2\right)}
\newcommand{\ioc}[2]{\left(#1, #2\right]} \newcommand{\ioc}[2]{\left(#1, #2\right]}
\newcommand{\ioo}[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$}}} \newcommand{\ubar}[1]{\text{\b{$#1$}}}
\let\oldemptyset\emptyset \let\oldemptyset\emptyset