diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 49f2d7d..e63d03e 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/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 diff --git a/Bookshelf/Enderton/Set/Chapter_1.lean b/Bookshelf/Enderton/Set/Chapter_1.lean index 9b9b89c..221b64e 100644 --- a/Bookshelf/Enderton/Set/Chapter_1.lean +++ b/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 \ No newline at end of file