Enderton, Baby Set Theory.

Bookshelf/Enderton/Set.tex

@@ -49,20 +49,23 @@ If $A$ and $B$ are sets such that for every object $t$,
 \section{Baby Set Theory}%
 \label{sec:baby-set-theory}
 
-\subsection{\partial{Exercise 1}}%
+\subsection{\verified{Exercise 1}}%
 \label{sub:baby-set-theory-1}
 
 Which of the following become true when "$\in$" is inserted in place of the
   blank?
 Which become true when "$\subseteq$" is inserted?
 
-\subsubsection{\partial{Exercise 1a}}%
+\subsubsection{\verified{Exercise 1a}}%
 \label{ssub:baby-set-theory-1a}
 
 $\{\emptyset\} \_\_\_\_ \{\emptyset, \{\emptyset\}\}$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_1a}
+
   Because the \textit{object} $\{\emptyset\}$ is a member of the right-hand set,
     the statement is \textbf{true} in the case of "$\in$".
 
@@ -72,13 +75,16 @@ $\{\emptyset\} \_\_\_\_ \{\emptyset, \{\emptyset\}\}$.
 
 \end{proof}
 
-\subsubsection{\partial{Exercise 1b}}%
+\subsubsection{\verified{Exercise 1b}}%
 \label{ssub:baby-set-theory-1b}
 
 $\{\emptyset\} \_\_\_\_ \{\emptyset, \{\{\emptyset\}\}\}$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_1b}
+
   Because the \textit{object} $\{\emptyset\}$ is not a member of the right-hand
     set, the statement is \textbf{false} in the case of "$\in$".
 
@@ -87,13 +93,16 @@ $\{\emptyset\} \_\_\_\_ \{\emptyset, \{\{\emptyset\}\}\}$.
 
 \end{proof}
 
-\subsubsection{\partial{Exercise 1c}}%
+\subsubsection{\verified{Exercise 1c}}%
 \label{ssub:baby-set-theory-1c}
 
 $\{\{\emptyset\}\} \_\_\_\_ \{\emptyset, \{\emptyset\}\}$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_1c}
+
   Because the \textit{object} $\{\{\emptyset\}\}$ is not a member of the
     right-hand set, the statement is \textbf{false} in the case of "$\in$".
 
@@ -102,13 +111,16 @@ $\{\{\emptyset\}\} \_\_\_\_ \{\emptyset, \{\emptyset\}\}$.
 
 \end{proof}
 
-\subsubsection{\partial{Exercise 1d}}%
+\subsubsection{\verified{Exercise 1d}}%
 \label{ssub:baby-set-theory-1d}
 
 $\{\{\emptyset\}\} \_\_\_\_ \{\emptyset, \{\{\emptyset\}\}\}$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_1d}
+
   Because the \textit{object} $\{\{\emptyset\}\}$ is a member of the right-hand
     set, the statement is \textbf{true} in the case of "$\in$".
 
@@ -118,13 +130,16 @@ $\{\{\emptyset\}\} \_\_\_\_ \{\emptyset, \{\{\emptyset\}\}\}$.
 
 \end{proof}
 
-\subsubsection{\partial{Exercise 1e}}%
+\subsubsection{\verified{Exercise 1e}}%
 \label{ssub:baby-set-theory-1e}
 
 $\{\{\emptyset\}\} \_\_ \{\emptyset, \{\emptyset, \{\emptyset\}\}\}$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_1e}
+
   Because the \textit{object} $\{\{\emptyset\}\}$ is not a member of the
     right-hand set, the statement is \textbf{false} in the case of "$\in$".
 
@@ -134,7 +149,7 @@ $\{\{\emptyset\}\} \_\_ \{\emptyset, \{\emptyset, \{\emptyset\}\}\}$.
 
 \end{proof}
 
-\subsection{\partial{Exercise 2}}%
+\subsection{\verified{Exercise 2}}%
 \label{sub:baby-set-theory-2}
 
 Show that no two of the three sets $\emptyset$, $\{\emptyset\}$, and
@@ -142,6 +157,9 @@ Show that no two of the three sets $\emptyset$, $\{\emptyset\}$, and
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_2}
+
   By the \nameref{ref:principle-extensionality}, $\emptyset$ is only equal to
     $\emptyset$.
   This immediately shows it is not equal to the other two.
@@ -153,13 +171,16 @@ Show that no two of the three sets $\emptyset$, $\{\emptyset\}$, and
 
 \end{proof}
 
-\subsection{\partial{Exercise 3}}%
+\subsection{\verified{Exercise 3}}%
 \label{sub:baby-set-theory-3}
 
 Show that if $B \subseteq C$, then $\mathscr{P} B \subseteq \mathscr{P} C$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_3}
+
   Let $x \in \mathscr{P} B$.
   By definition of the \nameref{ref:powerset}, $x$ is a subset of $B$.
   By hypothesis, $B \subseteq C$.
@@ -169,7 +190,7 @@ Show that if $B \subseteq C$, then $\mathscr{P} B \subseteq \mathscr{P} C$.
 
 \end{proof}
 
-\subsection{\partial{Exercise 4}}%
+\subsection{\verified{Exercise 4}}%
 \label{sub:baby-set-theory-4}
 
 Assume that $x$ and $y$ are members of a set $B$.
@@ -177,6 +198,9 @@ Show that $\{\{x\}, \{x, y\}\} \in \mathscr{P}\mathscr{P} B.$
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_1}
+    {Enderton.Set.Chapter\_1.exercise\_4}
+
   Let $x$ and $y$ be members of set $B$.
   Then $\{x\}$ and $\{x, y\}$ are subsets of $B$.
   By definition of the \nameref{ref:powerset}, $\{x\}$ and $\{x, y\}$ are

Bookshelf/Enderton/Set/Chapter_1.lean

@@ -1,4 +1,6 @@
 import Mathlib.Init.Set
+import Mathlib.Data.Set.Basic
+import Mathlib.Tactic.LibrarySearch
 
 /-! # Enderton.Chapter_1
 
@@ -7,7 +9,125 @@ Introduction
 
 namespace Enderton.Set.Chapter_1
 
+/-! ### Exercise 1
 
+Which of the following become true when "∈" is inserted in place of the blank?
+Which become true when "⊆" is inserted?
+-/
 
+/--
+The `∅` does not equal the singleton set containing `∅`.
+-/
+lemma empty_ne_singleton_empty (h : ∅ = ({∅} : Set (Set α))) : False :=
+  absurd h (Ne.symm $ Set.singleton_ne_empty (∅ : Set α))
+
+/-- #### Exercise 1a
+
+`{∅} ___ {∅, {∅}}`
+-/
+theorem exercise_1a
+  : {∅} ∈ ({∅, {∅}} : Set (Set (Set α)))
+  ∧ {∅} ⊆ ({∅, {∅}} : Set (Set (Set α))) := ⟨by simp, by simp⟩
+
+/-- #### Exercise 1b
+
+`{∅} ___ {∅, {{∅}}}`
+-/
+theorem exercise_1b
+  : {∅} ∉ ({∅, {{∅}}}: Set (Set (Set (Set α))))
+  ∧ {∅} ⊆ ({∅, {{∅}}}: Set (Set (Set (Set α)))) := by
+  refine ⟨?_, by simp⟩
+  intro h
+  simp at h
+  exact empty_ne_singleton_empty h
+
+/-- #### Exercise 1c
+
+`{{∅}} ___ {∅, {∅}}`
+-/
+theorem exercise_1c
+  : {{∅}} ∉ ({∅, {∅}} : Set (Set (Set (Set α))))
+  ∧ {{∅}} ⊆ ({∅, {∅}} : Set (Set (Set (Set α)))) := ⟨by simp, by simp⟩
+
+/-- #### Exercise 1d
+
+`{{∅}} ___ {∅, {{∅}}}`
+-/
+theorem exercise_1d
+  : {{∅}} ∈ ({∅, {{∅}}} : Set (Set (Set (Set α))))
+  ∧ ¬ {{∅}} ⊆ ({∅, {{∅}}} : Set (Set (Set (Set α)))) := by
+  refine ⟨by simp, ?_⟩
+  intro h
+  simp at h
+  exact empty_ne_singleton_empty h
+
+/-- #### Exercise 1e
+
+`{{∅}} ___ {∅, {∅, {∅}}}`
+-/
+theorem exercise_1e
+  : {{∅}} ∉ ({∅, {∅, {∅}}} : Set (Set (Set (Set α))))
+  ∧ ¬ {{∅}} ⊆ ({∅, {∅, {∅}}} : Set (Set (Set (Set α)))) := by
+  apply And.intro
+  · intro h
+    simp at h
+    rw [Set.ext_iff] at h
+    have nh := h ∅
+    simp at nh
+    exact empty_ne_singleton_empty nh
+  · intro h
+    simp at h
+    rw [Set.ext_iff] at h
+    have nh := h {∅}
+    simp at nh
+
+/-- ### Exercise 2
+
+Show that no two of the three sets `∅`, `{∅}`, and `{{∅}}` are equal to each
+other.
+-/
+theorem exercise_2
+  : ∅ ≠ ({∅} : Set (Set α))
+  ∧ ∅ ≠ ({{∅}} : Set (Set (Set α)))
+  ∧ {∅} ≠ ({{∅}} : Set (Set (Set α))) := by
+  refine ⟨?_, ⟨?_, ?_⟩⟩
+  · intro h
+    exact empty_ne_singleton_empty h
+  · intro h
+    exact absurd h (Ne.symm $ Set.singleton_ne_empty ({∅} : Set (Set α)))
+  · intro h
+    simp at h
+    exact empty_ne_singleton_empty h
+
+/-- ### Exercise 3
+
+Show that if `B ⊆ C`, then `𝓟 B ⊆ 𝓟 C`.
+-/
+theorem exercise_3 (h : B ⊆ C) : Set.powerset B ⊆ Set.powerset C := by
+  unfold Set.powerset
+  simp
+  intro x hx
+  exact Set.Subset.trans hx h
+
+/-- ### Exercise 4
+
+Assume that `x` and `y` are members of a set `B`. Show that
+`{{x}, {x, y}} ∈ 𝓟 𝓟 B`.
+-/
+theorem exercise_4 (x y : α) (hx : x ∈ B) (hy : y ∈ B)
+  : {{x}, {x, y}} ∈ Set.powerset (Set.powerset B) := by
+  unfold Set.powerset
+  simp only [Set.mem_singleton_iff, Set.mem_setOf_eq]
+  rw [Set.subset_def]
+  intro z hz
+  simp at hz
+  apply Or.elim hz
+  · intro h
+    rwa [h, Set.mem_setOf_eq, Set.singleton_subset_iff]
+  · intro h
+    rw [h, Set.mem_setOf_eq]
+    exact Set.union_subset
+      (Set.singleton_subset_iff.mpr hx)
+      (Set.singleton_subset_iff.mpr hy)
 
 end Enderton.Set.Chapter_1