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

Enderton. Continue actually verifying set theorems.

finite-set-exercises
Joshua Potter 2023-08-09 15:44:40 -06:00
parent 1eff704803
commit 83699dd58e
5 changed files with 494 additions and 82 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

125
Bookshelf/Enderton/Set.tex
View File

@ -1456,7 +1456,7 @@
Let $A$ and $B$ be sets. $x \not\in A + B$ if and only if either Let $A$ and $B$ be sets. $x \not\in A + B$ if and only if either
$x \in A \cap B$ or $x \not\in A \cup B$. $x \in A \cap B$ or $x \not\in A \cup B$.
\code*{Bookshelf/Enderton/Set/Basic} \code*{Common/Set/Basic}
{Set.not\_mem\_symm\_diff\_inter\_or\_not\_union} {Set.not\_mem\_symm\_diff\_inter\_or\_not\_union}
\begin{proof} \begin{proof}
@ -1948,7 +1948,7 @@
\end{align*} \end{align*}
\end{proof} \end{proof}
\subsection{\pending{Exercise 2.15a}}% \subsection{\verified{Exercise 2.15a}}%
\hyperlabel{sub:exercise-2.15a} \hyperlabel{sub:exercise-2.15a}
Show that $A \cap (B + C) = (A \cap B) + (A \cap C)$. Show that $A \cap (B + C) = (A \cap B) + (A \cap C)$.
@ -1956,6 +1956,9 @@
\lean*{Mathlib/Data/Set/Basic} \lean*{Mathlib/Data/Set/Basic}
{Set.inter\_symmDiff\_distrib\_left} {Set.inter\_symmDiff\_distrib\_left}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.exercise\_2\_15a}
\begin{proof} \begin{proof}
By definition of the intersection, \nameref{ref:symmetric-difference}, and By definition of the intersection, \nameref{ref:symmetric-difference}, and
relative complement of sets, relative complement of sets,
@ -1984,13 +1987,15 @@
\end{align*} \end{align*}
\end{proof} \end{proof}
\subsection{\pending{Exercise 2.15b}}% \subsection{\verified{Exercise 2.15b}}%
\hyperlabel{sub:exercise-2.15b} \hyperlabel{sub:exercise-2.15b}
Show that $A + (B + C) = (A + B) + C$. Show that $A + (B + C) = (A + B) + C$.
\lean*{Mathlib/Data/Set/Basic} \lean*{Mathlib/Order/SymmDiff}{symmDiff\_assoc}
{Set.symmDiff\_assoc}
\code{Bookshelf/Enderton/Set/Chapter\_2}
{Enderton.Set.Chapter\_2.exercise\_2\_15b}
\begin{proof} \begin{proof}
Let $A$, $B$, and $C$ be sets. Let $A$, $B$, and $C$ be sets.
@ -2658,11 +2663,6 @@
pairs $\pair{x, y}$ with $x \in A$ and $y \in B$. pairs $\pair{x, y}$ with $x \in A$ and $y \in B$.
\end{theorem} \end{theorem}
\begin{note}
The below Lean proof is a definition (i.e. an axiom).
It does not prove such a set's existence from first principles.
\end{note}
\lean{Mathlib/SetTheory/ZFC/Basic}{Set.prod} \lean{Mathlib/SetTheory/ZFC/Basic}{Set.prod}
\begin{proof} \begin{proof}
@ -2830,7 +2830,7 @@
\hyperlabel{sub:lemma-1} \hyperlabel{sub:lemma-1}
\hyperlabel{sub:one-to-one-inverse} \hyperlabel{sub:one-to-one-inverse}
\begin{lemma} \begin{lemma}[1]
For any one-to-one function $F$, $F^{-1}$ is also one-to-one. For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
\end{lemma} \end{lemma}
@ -3985,7 +3985,7 @@
showing it can be represented as an ordered $1$-tuple as well. showing it can be represented as an ordered $1$-tuple as well.
\end{answer} \end{answer}
\subsection{\pending{Exercise 3.11}}% \subsection{\unverified{Exercise 3.11}}%
\hyperlabel{sub:exercise-3.11} \hyperlabel{sub:exercise-3.11}
Prove the following version (for functions) of the extensionality principle: Prove the following version (for functions) of the extensionality principle:
@ -6083,7 +6083,7 @@
\section{Arithmetic}% \section{Arithmetic}%
\hyperlabel{sec:arithmetic} \hyperlabel{sec:arithmetic}
\subsection{\pending{Theorem 4I}} \subsection{\verified{Theorem 4I}}
\hyperlabel{sub:theorem-4i} \hyperlabel{sub:theorem-4i}
\begin{theorem}[4I] \begin{theorem}[4I]
@ -6098,6 +6098,9 @@
\lean{Init/Prelude}{Nat.add} \lean{Init/Prelude}{Nat.add}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4i}
\begin{proof} \begin{proof}
\paragraph{\eqref{sub:theorem-4i-eq1}}% \paragraph{\eqref{sub:theorem-4i-eq1}}%
@ -6115,7 +6118,7 @@
\end{proof} \end{proof}
\subsection{\pending{Theorem 4J}} \subsection{\verified{Theorem 4J}}
\hyperlabel{sub:theorem-4j} \hyperlabel{sub:theorem-4j}
\begin{theorem}[4J] \begin{theorem}[4J]
@ -6130,6 +6133,9 @@
\lean{Init/Prelude}{Nat.mul} \lean{Init/Prelude}{Nat.mul}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4j}
\begin{proof} \begin{proof}
\paragraph{\eqref{sub:theorem-4j-eq1}}% \paragraph{\eqref{sub:theorem-4j-eq1}}%
@ -6145,7 +6151,7 @@
\end{proof} \end{proof}
\subsection{\pending{Left Additive Identity}}% \subsection{\verified{Left Additive Identity}}%
\hyperlabel{sub:left-additive-identity} \hyperlabel{sub:left-additive-identity}
\begin{lemma} \begin{lemma}
@ -6155,6 +6161,9 @@
\lean{Init/Data/Nat/Basic}{Nat.zero\_add} \lean{Init/Data/Nat/Basic}{Nat.zero\_add}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.left\_additive\_identity}
\begin{proof} \begin{proof}
Let $S = \{n \in \omega \mid 0 + n = n\}$. Let $S = \{n \in \omega \mid 0 + n = n\}$.
@ -6185,17 +6194,20 @@
\end{proof} \end{proof}
\subsection{\pending{Lemma 3}}% \subsection{\verified{Lemma 2}}%
\hyperlabel{sub:lemma-3} \hyperlabel{sub:lemma-2}
\hyperlabel{sub:succ-add-eq-add-succ} \hyperlabel{sub:succ-add-eq-add-succ}
\begin{lemma} \begin{lemma}[2]
For all $m, n \in \omega$, $A_{m^+}(n) = A_m(n^+)$. For all $m, n \in \omega$, $A_{m^+}(n) = A_m(n^+)$.
In other words, $$m^+ + n = m + n^+.$$ In other words, $$m^+ + n = m + n^+.$$
\end{lemma} \end{lemma}
\lean{Std/Data/Nat/Lemmas}{Nat.succ\_add\_eq\_succ\_add} \lean{Std/Data/Nat/Lemmas}{Nat.succ\_add\_eq\_succ\_add}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.lemma\_2}
\begin{proof} \begin{proof}
Let $m \in \omega$ and define Let $m \in \omega$ and define
@ -6204,14 +6216,14 @@
Afterwards we show that (iii) our theorem holds. Afterwards we show that (iii) our theorem holds.
\paragraph{(i)}% \paragraph{(i)}%
\hyperlabel{par:lemma-3-i} \hyperlabel{par:lemma-2-i}
By \nameref{sub:theorem-4i}, $m^+ + 0 = m^+$. By \nameref{sub:theorem-4i}, $m^+ + 0 = m^+$.
Likewise, $m + 0^+ = (m + 0)^+ = m^+$. Likewise, $m + 0^+ = (m + 0)^+ = m^+$.
Thus $0 \in S$. Thus $0 \in S$.
\paragraph{(ii)}% \paragraph{(ii)}%
\hyperlabel{par:lemma-3-ii} \hyperlabel{par:lemma-2-ii}
Suppose $n \in S$. Suppose $n \in S$.
By \nameref{sub:theorem-4i}, $m^+ + n^+ = (m^+ + n)^+$. By \nameref{sub:theorem-4i}, $m^+ + n^+ = (m^+ + n)^+$.
@ -6221,13 +6233,13 @@
\paragraph{(iii)}% \paragraph{(iii)}%
By \nameref{par:lemma-3-i} and \nameref{par:lemma-3-ii}, $S$ is inductive. By \nameref{par:lemma-2-i} and \nameref{par:lemma-2-ii}, $S$ is inductive.
Hence \nameref{sub:theorem-4b} implies $S = \omega$. Hence \nameref{sub:theorem-4b} implies $S = \omega$.
Thus for all $n \in \omega$, $m^+ + n = m + n^+$. Thus for all $n \in \omega$, $m^+ + n = m + n^+$.
\end{proof} \end{proof}
\subsection{\pending{Theorem 4K-1}}% \subsection{\verified{Theorem 4K-1}}%
\hyperlabel{sub:theorem-4k-1} \hyperlabel{sub:theorem-4k-1}
\begin{theorem}[4K-1] \begin{theorem}[4K-1]
@ -6235,7 +6247,10 @@
For $m, n, p \in \omega$, $$m + (n + p) = (m + n) + p.$$ For $m, n, p \in \omega$, $$m + (n + p) = (m + n) + p.$$
\end{theorem} \end{theorem}
\lean{Mathlib/Algebra/Group/Defs}{add\_assoc} \lean{Init/Data/Nat/Basic}{Nat.add\_assoc}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_1}
\begin{proof} \begin{proof}
@ -6281,7 +6296,7 @@
\end{proof} \end{proof}
\subsection{\pending{Theorem 4K-2}}% \subsection{\verified{Theorem 4K-2}}%
\hyperlabel{sub:theorem-4k-2} \hyperlabel{sub:theorem-4k-2}
\begin{theorem}[4K-2] \begin{theorem}[4K-2]
@ -6289,7 +6304,10 @@
For $m, n \in \omega$, $$m + n = n + m.$$ For $m, n \in \omega$, $$m + n = n + m.$$
\end{theorem} \end{theorem}
\lean{Mathlib/Algebra/Group/Defs}{add\_comm} \lean{Init/Data/Nat/Basic}{Nat.add\_comm}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_2}
\begin{proof} \begin{proof}
@ -6331,7 +6349,7 @@
\end{proof} \end{proof}
\subsection{\pending{Zero Multiplicand}}% \subsection{\verified{Zero Multiplicand}}%
\hyperlabel{sub:zero-multiplicand} \hyperlabel{sub:zero-multiplicand}
\begin{lemma} \begin{lemma}
@ -6341,6 +6359,9 @@
\lean{Init/Data/Nat/Basic}{Nat.zero\_mul} \lean{Init/Data/Nat/Basic}{Nat.zero\_mul}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.zero\_multiplicand}
\begin{proof} \begin{proof}
Define Define
@ -6365,8 +6386,8 @@
\begin{align*} \begin{align*}
0 \cdot n^+ 0 \cdot n^+
& = 0 \cdot n + 0 & \textref{sub:theorem-4j} \\ & = 0 \cdot n + 0 & \textref{sub:theorem-4j} \\
& = 0 + 0 & \eqref{sub:zero-multiplicand-eq1} \\ & = 0 \cdot n & \textref{sub:theorem-4i} \\
& = 0. & \textref{ref:addition} & = 0. & \eqref{sub:zero-multiplicand-eq1}
\end{align*} \end{align*}
Thus $n^+ \in S$. Thus $n^+ \in S$.
@ -6380,7 +6401,7 @@
\end{proof} \end{proof}
\subsection{\pending{Successor Distribution}}% \subsection{\verified{Successor Distribution}}%
\hyperlabel{sub:successor-distribution} \hyperlabel{sub:successor-distribution}
\begin{lemma} \begin{lemma}
@ -6390,6 +6411,9 @@
\lean{Init/Data/Nat/Basic}{Nat.succ\_mul} \lean{Init/Data/Nat/Basic}{Nat.succ\_mul}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.succ\_distrib}
\begin{proof} \begin{proof}
Let $m \in \omega$ and define Let $m \in \omega$ and define
@ -6434,7 +6458,7 @@
\end{proof} \end{proof}
\subsection{\pending{Theorem 4K-3}} \subsection{\verified{Theorem 4K-3}}
\hyperlabel{sub:theorem-4k-3} \hyperlabel{sub:theorem-4k-3}
\begin{theorem}[4K-3] \begin{theorem}[4K-3]
@ -6444,6 +6468,9 @@
\lean{Init/Data/Nat/Basic}{Nat.left\_distrib} \lean{Init/Data/Nat/Basic}{Nat.left\_distrib}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_3}
\begin{proof} \begin{proof}
Fix $n, p \in \omega$ and define Fix $n, p \in \omega$ and define
@ -6494,7 +6521,7 @@
\end{proof} \end{proof}
\subsection{\pending{Successor Identity}}% \subsection{\verified{Successor Identity}}%
\hyperlabel{sub:successor-identity} \hyperlabel{sub:successor-identity}
\begin{lemma} \begin{lemma}
@ -6504,6 +6531,9 @@
\lean{Std/Data/Nat/Lemmas}{Nat.succ\_eq\_one\_add} \lean{Std/Data/Nat/Lemmas}{Nat.succ\_eq\_one\_add}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.succ\_identity}
\begin{proof} \begin{proof}
Let Let
@ -6545,7 +6575,7 @@
\end{proof} \end{proof}
\subsection{\pending{Right Multiplicative Identity}}% \subsection{\verified{Right Multiplicative Identity}}%
\hyperlabel{sub:right-multiplicative-identity} \hyperlabel{sub:right-multiplicative-identity}
\begin{lemma} \begin{lemma}
@ -6553,7 +6583,10 @@
In other words, $$m \cdot 1 = m.$$ In other words, $$m \cdot 1 = m.$$
\end{lemma} \end{lemma}
\lean{Init/Data/Nat/Basic}{mul\_one} \lean{Init/Data/Nat/Basic}{Nat.mul\_one}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.right\_mul\_id}
\begin{proof} \begin{proof}
@ -6594,7 +6627,7 @@
\end{proof} \end{proof}
\subsection{\pending{Theorem 4K-5}} \subsection{\verified{Theorem 4K-5}}
\hyperlabel{sub:theorem-4k-5} \hyperlabel{sub:theorem-4k-5}
\begin{theorem}[4K-5] \begin{theorem}[4K-5]
@ -6607,7 +6640,10 @@
two properties in the opposite direction. two properties in the opposite direction.
\end{note} \end{note}
\lean{Mathlib/Algebra/Group/Defs}{mul\_comm} \lean{Init/Data/Nat/Basic}{Nat.mul\_comm}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_5}
\begin{proof} \begin{proof}
@ -6652,7 +6688,7 @@
\end{proof} \end{proof}
\subsection{\pending{Theorem 4K-4}}% \subsection{\verified{Theorem 4K-4}}%
\hyperlabel{sub:theorem-4k-4} \hyperlabel{sub:theorem-4k-4}
\begin{theorem}[4K-4] \begin{theorem}[4K-4]
@ -6660,7 +6696,10 @@
For $m, n, p \in \omega$, $$m \cdot (n \cdot p) = (m \cdot n) \cdot p.$$ For $m, n, p \in \omega$, $$m \cdot (n \cdot p) = (m \cdot n) \cdot p.$$
\end{theorem} \end{theorem}
\lean{Mathlib/Algebra/Group/Defs}{mul\_assoc} \lean{Init/Data/Nat/Basic}{Nat.mul\_assoc}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4k\_4}
\begin{proof} \begin{proof}
@ -6708,7 +6747,7 @@
\section{Ordering on \texorpdfstring{$\omega$}{Natural Numbers}}% \section{Ordering on \texorpdfstring{$\omega$}{Natural Numbers}}%
\hyperlabel{sec:ordering-natural-numbers} \hyperlabel{sec:ordering-natural-numbers}
\subsection{\pending{Ordering on Successor}}% \subsection{\unverified{Ordering on Successor}}%
\hyperlabel{sub:ordering-successor} \hyperlabel{sub:ordering-successor}
\begin{lemma} \begin{lemma}
@ -6746,7 +6785,7 @@
Thus $m \in n \iff m \in \omega \land m \in n$. Thus $m \in n \iff m \in \omega \land m \in n$.
\end{proof} \end{proof}
\subsection{\pending{Lemma 4L(a)}}% \subsection{\unverified{Lemma 4L(a)}}%
\hyperlabel{sub:lemma-4l-a} \hyperlabel{sub:lemma-4l-a}
\begin{lemma}[4L(a)] \begin{lemma}[4L(a)]
@ -6804,8 +6843,7 @@
Suppose $m^+ \in n^+$. Suppose $m^+ \in n^+$.
The definition of \nameref{ref:successor} immediately implies that The definition of \nameref{ref:successor} immediately implies that
$m \in m^+$. $m \in m^+$.
By \nameref{sec:ordering-natural-numbers}, $m^+ \in n^+$ implies Likewise, $m^+ \in n^+$ implies $m^+ \in n$ or $m^+ = n$.
$m^+ \in n$ or $m^+ = n$.
If the latter, $m \in n$ immediately follows. If the latter, $m \in n$ immediately follows.
If the former, we note $n$ is a transitive set by If the former, we note $n$ is a transitive set by
\nameref{sub:theorem-4f}. \nameref{sub:theorem-4f}.
@ -6813,7 +6851,7 @@
\end{proof} \end{proof}
\subsection{\pending{Lemma 4L(b)}}% \subsection{\verified{Lemma 4L(b)}}%
\hyperlabel{sub:lemma-4l-b} \hyperlabel{sub:lemma-4l-b}
\begin{lemma}[4L(b)] \begin{lemma}[4L(b)]
@ -6822,6 +6860,9 @@
\lean{Init/Prelude}{Nat.lt\_irrefl} \lean{Init/Prelude}{Nat.lt\_irrefl}
\code{Bookshelf/Enderton/Set/Chapter\_4}
{Enderton.Set.Chapter\_4.theorem\_4l\_b}
\begin{proof} \begin{proof}
Define Define

87
Bookshelf/Enderton/Set/Chapter_2.lean
View File

@ -1,6 +1,7 @@
import Bookshelf.Enderton.Set.Chapter_1 import Bookshelf.Enderton.Set.Chapter_1
import Common.Set.Basic import Common.Set.Basic
import Mathlib.Data.Set.Lattice import Mathlib.Data.Set.Lattice
import Mathlib.Order.SymmDiff
/-! # Enderton.Set.Chapter_2 /-! # Enderton.Set.Chapter_2
@ -261,7 +262,7 @@ theorem anti_monotonicity_ii (A B : Set (Set α)) (h : A ⊆ B)
#check Set.sInter_subset_sInter #check Set.sInter_subset_sInter
/-- #### ∩/- Associativity /-- #### Intersection/Difference Associativity
Let `A`, `B`, and `C` be sets. Then `A ∩ (B - C) = (A ∩ B) - C`. Let `A`, `B`, and `C` be sets. Then `A ∩ (B - C) = (A ∩ B) - C`.
-/ -/
@ -271,7 +272,8 @@ theorem inter_diff_assoc (A B C : Set α)
_ = { x | x ∈ A ∧ (x ∈ B ∧ x ∉ C) } := rfl _ = { x | x ∈ A ∧ (x ∈ B ∧ x ∉ C) } := rfl
_ = { x | (x ∈ A ∧ x ∈ B) ∧ x ∉ C } := by _ = { x | (x ∈ A ∧ x ∈ B) ∧ x ∉ C } := by
ext _ ext _
sorry simp only [Set.mem_setOf_eq]
rw [and_assoc]
_ = { x | x ∈ A ∩ B ∧ x ∉ C } := rfl _ = { x | x ∈ A ∩ B ∧ x ∉ C } := rfl
_ = (A ∩ B) \ C := rfl _ = (A ∩ B) \ C := rfl
@ -667,6 +669,87 @@ theorem exercise_2_14 : A \ (B \ C) ≠ (A \ B) \ C := by
end end
/-- #### Exercise 2.15 (a)
Show that `A ∩ (B + C) = (A ∩ B) + (A ∩ C)`.
-/
theorem exercise_2_15a (A B C : Set α)
: A ∩ (B ∆ C) = (A ∩ B) ∆ (A ∩ C) := Eq.symm $
calc (A ∩ B) ∆ (A ∩ C)
_ = ((A ∩ B) \ (A ∩ C)) ∪ ((A ∩ C) \ (A ∩ B)) := rfl
_ = ((A ∩ B) \ A) ∪
((A ∩ B) \ C) ∪
(((A ∩ C) \ A) ∪
((A ∩ C) \ B)) := by
iterate 2 rw [Set.diff_inter]
_ = (A ∩ (B \ A)) ∪
(A ∩ (B \ C)) ∪
((A ∩ (C \ A)) ∪
(A ∩ (C \ B))) := by
iterate 4 rw [Set.inter_diff_assoc]
_ = ∅ ∪ (A ∩ (B \ C)) ∪ (∅ ∪ (A ∩ (C \ B))) := by
iterate 2 rw [Set.inter_diff_self]
_ = (A ∩ (B \ C)) ∪ (A ∩ (C \ B)) := by
simp only [Set.empty_union]
_ = A ∩ ((B \ C) ∪ (C \ B)) := by
rw [Set.inter_distrib_left]
_ = A ∩ (B ∆ C) := rfl
#check Set.inter_symmDiff_distrib_left
/-- #### Exercise 2.15 (b)
Show that `A + (B + C) = (A + B) + C`.
-/
theorem exercise_2_15b (A B C : Set α)
: A ∆ (B ∆ C) = (A ∆ B) ∆ C := by
rw [Set.Subset.antisymm_iff]
apply And.intro
· show ∀ x, x ∈ A ∆ (B ∆ C) → x ∈ (A ∆ B) ∆ C
intro x hx
apply Or.elim hx
· intro ⟨hA, nBC⟩
rw [Set.not_mem_symm_diff_inter_or_not_union] at nBC
apply Or.elim nBC
· intro h
have : x ∉ A ∆ B := Set.symm_diff_mem_both_not_mem hA h.left
exact Set.symm_diff_mem_right this h.right
· intro h
have ⟨nB, nC⟩ : x ∉ B ∧ x ∉ C := not_or_de_morgan.mp h
have : x ∈ A ∆ B := Set.symm_diff_mem_left hA nB
exact Set.symm_diff_mem_left this nC
· intro ⟨hx₁, hx₂⟩
apply Or.elim hx₁
· intro ⟨hB, nC⟩
have : x ∈ A ∆ B := Set.symm_diff_mem_right hx₂ hB
exact Set.symm_diff_mem_left this nC
· intro ⟨hC, nB⟩
have : x ∉ A ∆ B := Set.symm_diff_not_mem_both_not_mem hx₂ nB
exact Set.symm_diff_mem_right this hC
· show ∀ x, x ∈ (A ∆ B) ∆ C → x ∈ A ∆ (B ∆ C)
intro x hx
apply Or.elim hx
· intro ⟨hAB, nC⟩
apply Or.elim hAB
· intro ⟨hA, nB⟩
have : x ∉ B ∆ C := Set.symm_diff_not_mem_both_not_mem nB nC
exact Set.symm_diff_mem_left hA this
· intro ⟨hB, nA⟩
have : x ∈ B ∆ C := Set.symm_diff_mem_left hB nC
exact Set.symm_diff_mem_right nA this
· intro ⟨hC, nAB⟩
rw [Set.not_mem_symm_diff_inter_or_not_union] at nAB
apply Or.elim nAB
· intro ⟨hA, hB⟩
have : x ∉ B ∆ C := Set.symm_diff_mem_both_not_mem hB hC
exact Set.symm_diff_mem_left hA this
· intro h
have ⟨nA, nB⟩ : x ∉ A ∧ x ∉ B := not_or_de_morgan.mp h
have : x ∈ B ∆ C := Set.symm_diff_mem_right nB hC
exact Set.symm_diff_mem_right nA this
#check symmDiff_assoc
/-- #### Exercise 2.16 /-- #### Exercise 2.16
Simplify: Simplify:

2
Bookshelf/Enderton/Set/Chapter_3.lean
View File

@ -19,7 +19,7 @@ namespace Enderton.Set.Chapter_3
If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`. If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`.
-/ -/
theorem lemma_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C) lemma lemma_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
: OrderedPair x y ∈ 𝒫 𝒫 C := by : OrderedPair x y ∈ 𝒫 𝒫 C := by
have hxs : {x} ⊆ C := Set.singleton_subset_iff.mpr hx have hxs : {x} ⊆ C := Set.singleton_subset_iff.mpr hx
have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy

322
Bookshelf/Enderton/Set/Chapter_4.lean
View File

@ -18,6 +18,291 @@ theorem theorem_4c (n : ℕ)
| 0 => simp | 0 => simp
| m + 1 => simp | m + 1 => simp
#check Nat.exists_eq_succ_of_ne_zero
/-- #### Theorem 4I
For natural numbers `m` and `n`,
```
m + 0 = m,
m + n⁺ = (m + n)⁺
```
-/
theorem theorem_4i (m n : ℕ)
: m + 0 = m ∧ m + n.succ = (m + n).succ := ⟨rfl, rfl⟩
/-- #### Theorem 4J
For natural numbers `m` and `n`,
```
m ⬝ 0 = 0,
m ⬝ n⁺ = m ⬝ n + m .
```
-/
theorem theorem_4j (m n : ℕ)
: m * 0 = 0 ∧ m * n.succ = m * n + m := ⟨rfl, rfl⟩
/-- #### Left Additive Identity
For all `n ∈ ω`, `A₀(n) = n`. In other words, `0 + n = n`.
-/
lemma left_additive_identity (n : ℕ)
: 0 + n = n := by
induction n with
| zero => simp
| succ n ih =>
calc 0 + n.succ
_ = (0 + n).succ := rfl
_ = n.succ := by rw [ih]
#check Nat.zero_add
/-- #### Lemma 2
For all `m, n ∈ ω`, `Aₘ₊(n) = Aₘ(n⁺)`. In other words, `m⁺ + n = m + n⁺`.
-/
lemma lemma_2 (m n : ℕ)
: m.succ + n = m + n.succ := by
induction n with
| zero => rfl
| succ n ih =>
calc m.succ + n.succ
_ = (m.succ + n).succ := rfl
_ = (m + n.succ).succ := by rw [ih]
_ = m + n.succ.succ := rfl
#check Nat.succ_add_eq_succ_add
/-- #### Theorem 4K-1
Associatve law for addition. For `m, n, p ∈ ω`,
```
m + (n + p) = (m + n) + p.
```
-/
theorem theorem_4k_1 (m n p : ℕ)
: m + (n + p) = (m + n) + p := by
induction m with
| zero => simp
| succ m ih =>
calc m.succ + (n + p)
_ = m + (n + p).succ := by rw [lemma_2]
_ = (m + (n + p)).succ := rfl
_ = ((m + n) + p).succ := by rw [ih]
_ = (m + n) + p.succ := rfl
_ = (m + n).succ + p := by rw [lemma_2]
_ = (m + n.succ) + p := rfl
_ = (m.succ + n) + p := by rw [lemma_2]
#check Nat.add_assoc
/-- #### Theorem 4K-2
Commutative law for addition. For `m, n ∈ ω`,
```
m + n = n + m.
```
-/
theorem theorem_4k_2 {m n : ℕ}
: m + n = n + m := by
induction m with
| zero => simp
| succ m ih =>
calc m.succ + n
_ = m + n.succ := by rw [lemma_2]
_ = (m + n).succ := rfl
_ = (n + m).succ := by rw [ih]
_ = n + m.succ := by rfl
#check Nat.add_comm
/-- #### Zero Multiplicand
For all `n ∈ ω`, `M₀(n) = 0`. In other words, `0 ⬝ n = 0`.
-/
theorem zero_multiplicand (n : ℕ)
: 0 * n = 0 := by
induction n with
| zero => simp
| succ n ih =>
calc 0 * n.succ
_ = 0 * n + 0 := rfl
_ = 0 * n := rfl
_ = 0 := by rw [ih]
#check Nat.zero_mul
/-- #### Successor Distribution
For all `m, n ∈ ω`, `Mₘ₊(n) = Mₘ(n) + n`. In other words,
```
m⁺ ⬝ n = m ⬝ n + n.
```
-/
theorem succ_distrib (m n : ℕ)
: m.succ * n = m * n + n := by
induction n with
| zero => simp
| succ n ih =>
calc m.succ * n.succ
_ = m.succ * n + m.succ := rfl
_ = (m * n + n) + m.succ := by rw [ih]
_ = m * n + (n + m.succ) := by rw [theorem_4k_1]
_ = m * n + (n.succ + m) := by rw [lemma_2]
_ = m * n + (m + n.succ) := by
conv => left; arg 2; rw [theorem_4k_2]
_ = (m * n + m) + n.succ := by rw [theorem_4k_1]
_ = m * n.succ + n.succ := rfl
#check Nat.succ_mul
/-- #### Theorem 4K-3
Distributive law. For `m, n, p ∈ ω`,
```
m ⬝ (n + p) = m ⬝ n + m ⬝ p.
```
-/
theorem theorem_4k_3 (m n p : ℕ)
: m * (n + p) = m * n + m * p := by
induction m with
| zero => simp
| succ m ih =>
calc m.succ * (n + p)
_ = m * (n + p) + (n + p) := by rw [succ_distrib]
_ = m * (n + p) + n + p := by rw [← theorem_4k_1]
_ = m * n + m * p + n + p := by rw [ih]
_ = m * n + (m * p + n) + p := by rw [theorem_4k_1]
_ = m * n + (n + m * p) + p := by
conv => left; arg 1; arg 2; rw [theorem_4k_2]
_ = (m * n + n) + (m * p + p) := by rw [theorem_4k_1, theorem_4k_1]
_ = m.succ * n + m.succ * p := by rw [succ_distrib, succ_distrib]
/-- #### Successor Identity
For all `m ∈ ω`, `Aₘ(1) = m⁺`. In other words, `m + 1 = m⁺`.
-/
theorem succ_identity (m : ℕ)
: m + 1 = m.succ := by
induction m with
| zero => simp
| succ m ih =>
calc m.succ + 1
_ = m + (Nat.succ Nat.zero).succ := by rw [lemma_2]
_ = (m + 1).succ := rfl
_ = m.succ.succ := by rw [ih]
#check Nat.succ_eq_one_add
/-- #### Right Multiplicative Identity
For all `m ∈ ω`, `Mₘ(1) = m`. In other words, `m ⬝ 1 = m`.
-/
theorem right_mul_id (m : ℕ)
: m * 1 = m := by
induction m with
| zero => simp
| succ m ih =>
calc m.succ * 1
_ = m * 1 + 1 := by rw [succ_distrib]
_ = m + 1 := by rw [ih]
_ = m.succ := by rw [succ_identity]
#check Nat.mul_one
/-- #### Theorem 4K-5
Commutative law for multiplication. For `m, n ∈ ω`, `m ⬝ n = n ⬝ m`.
-/
theorem theorem_4k_5 (m n : ℕ)
: m * n = n * m := by
induction m with
| zero => simp
| succ m ih =>
calc m.succ * n
_ = m * n + n := by rw [succ_distrib]
_ = n * m + n := by rw [ih]
_ = n * m + n * 1 := by
conv => left; arg 2; rw [← right_mul_id n]
_ = n * (m + 1) := by rw [← theorem_4k_3]
_ = n * m.succ := by rw [succ_identity]
#check Nat.mul_comm
/-- #### Theorem 4K-4
Associative law for multiplication. For `m, n, p ∈ ω`,
```
m ⬝ (n ⬝ p) = (m ⬝ n) ⬝ p.
```
-/
theorem theorem_4k_4 (m n p : ℕ)
: m * (n * p) = (m * n) * p := by
induction p with
| zero => simp
| succ p ih =>
calc m * (n * p.succ)
_ = m * (n * p + n) := rfl
_ = m * (n * p) + m * n := by rw [theorem_4k_3]
_ = (m * n) * p + m * n := by rw [ih]
_ = p * (m * n) + m * n := by rw [theorem_4k_5]
_ = p.succ * (m * n) := by rw [succ_distrib]
_ = (m * n) * p.succ := by rw [theorem_4k_5]
#check Nat.mul_assoc
/-- #### Lemma 4L(b)
No natural number is a member of itself.
-/
lemma lemma_4l_b (n : ℕ)
: ¬ n < n := by
induction n with
| zero => simp
| succ n ih =>
by_contra nh
rw [Nat.succ_lt_succ_iff] at nh
exact absurd nh ih
#check Nat.lt_irrefl
/-- #### Lemma 10
For every natural number `n ≠ 0`, `0 ∈ n`.
-/
theorem zero_least_nat (n : ℕ)
: 0 = n ∨ 0 < n := by
by_cases h : n = 0
· left
rw [h]
· right
have ⟨m, hm⟩ := Nat.exists_eq_succ_of_ne_zero h
rw [hm]
exact Nat.succ_pos m
/-- #### Trichotomy Law for ω
For any natural numbers `m` and `n`, exactly one of the three conditions
```
m ∈ n, m = n, n ∈ m
```
holds.
-/
theorem trichotomy_law_for_nat
: IsAsymm ℕ LT.lt ∧ IsTrichotomous ℕ LT.lt :=
⟨instIsAsymmLtToLT, instIsTrichotomousLtToLTToPreorderToPartialOrder⟩
/-- #### Linear Ordering on ω
Relation
```
∈_ω = {⟨m, n⟩ ∈ ω × ω | m ∈ n}
```
is a linear ordering on `ω`.
-/
theorem linear_ordering_on_nat
: IsStrictTotalOrder ℕ LT.lt := isStrictTotalOrder_of_linearOrder
/-- #### Exercise 4.1 /-- #### Exercise 4.1
Show that `1 ≠ 3` i.e., that `∅⁺ ≠ ∅⁺⁺⁺`. Show that `1 ≠ 3` i.e., that `∅⁺ ≠ ∅⁺⁺⁺`.
@ -105,41 +390,4 @@ theorem exercise_4_14 (n : ℕ)
have : even n := ⟨q, hq'⟩ have : even n := ⟨q, hq'⟩
exact absurd this h exact absurd this h
/-- #### Lemma 10
For every natural number `n ≠ 0`, `0 ∈ n`.
-/
theorem zero_least_nat (n : ℕ)
: 0 = n ∨ 0 < n := by
by_cases h : n = 0
· left
rw [h]
· right
have ⟨m, hm⟩ := Nat.exists_eq_succ_of_ne_zero h
rw [hm]
exact Nat.succ_pos m
/-- #### Trichotomy Law for ω
For any natural numbers `m` and `n`, exactly one of the three conditions
```
m ∈ n, m = n, n ∈ m
```
holds.
-/
theorem trichotomy_law_for_nat
: IsAsymm ℕ LT.lt ∧ IsTrichotomous ℕ LT.lt :=
⟨instIsAsymmLtToLT, instIsTrichotomousLtToLTToPreorderToPartialOrder⟩
/-- #### Linear Ordering on ω
Relation
```
∈_ω = {⟨m, n⟩ ∈ ω × ω | m ∈ n}
```
is a linear ordering on `ω`.
-/
theorem linear_ordering_on_nat
: IsStrictTotalOrder ℕ LT.lt := isStrictTotalOrder_of_linearOrder
end Enderton.Set.Chapter_4 end Enderton.Set.Chapter_4

40
Common/Set/Basic.lean
View File

@ -156,6 +156,46 @@ theorem prod_nonempty_nonempty_imp_nonempty_prod {A : Set α} {B : Set β}
/-! ## Symmetric Difference -/ /-! ## Symmetric Difference -/
/--
If `x ∈ A` and `x ∉ B`, then `x ∈ A ∆ B`.
-/
theorem symm_diff_mem_left {A B : Set α} (hA : x ∈ A) (hB : x ∉ B)
: x ∈ A ∆ B := by
left
exact ⟨hA, hB⟩
/--
If `x ∉ A` and `x ∈ B`, then `x ∈ A ∆ B`.
-/
theorem symm_diff_mem_right {A B : Set α} (hA : x ∉ A) (hB : x ∈ B)
: x ∈ A ∆ B := by
right
exact ⟨hB, hA⟩
/--
If `x ∈ A` and `x ∈ B`, then `x ∉ A ∆ B`.
-/
theorem symm_diff_mem_both_not_mem {A B : Set α} (hA : x ∈ A) (hB : x ∈ B)
: x ∉ A ∆ B := by
intro h
apply Or.elim h
· intro ⟨_, nB⟩
exact absurd hB nB
· intro ⟨_, nA⟩
exact absurd hA nA
/--
If `x ∉ A` and `x ∉ B`, then `x ∉ A ∆ B`.
-/
theorem symm_diff_not_mem_both_not_mem {A B : Set α} (nA : x ∉ A) (nB : x ∉ B)
: x ∉ A ∆ B := by
intro h
apply Or.elim h
· intro ⟨hA, _⟩
exact absurd hA nA
· intro ⟨hB, _⟩
exact absurd hB nB
/-- /--
`x` is a member of the `symmDiff` of `A` and `B` **iff** `x ∈ A ∧ x ∉ B` or `x` is a member of the `symmDiff` of `A` and `B` **iff** `x ∈ A ∧ x ∉ B` or
`x ∉ A ∧ x ∈ B`. `x ∉ A ∧ x ∈ B`.