diff --git a/Bookshelf/Enderton/Set.lean b/Bookshelf/Enderton/Set.lean index 231a644..e1d66fd 100644 --- a/Bookshelf/Enderton/Set.lean +++ b/Bookshelf/Enderton/Set.lean @@ -1,3 +1,5 @@ import Bookshelf.Enderton.Set.Chapter_1 import Bookshelf.Enderton.Set.Chapter_2 -import Bookshelf.Enderton.Set.Chapter_3 \ No newline at end of file +import Bookshelf.Enderton.Set.Chapter_3 +import Bookshelf.Enderton.Set.OrderedPair +import Bookshelf.Enderton.Set.Relation \ No newline at end of file diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 5d615ee..5caf9ce 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -73,6 +73,12 @@ There is a set having no members: \end{axiom} +\section{\partial{Equivalence Relation}}% +\label{ref:equivalence-relation} + +Relation $R$ is an \textbf{equivalence relation} if and only if $R$ is a binary + relation that is reflexive, symmetric, and transitive. + \section{\defined{Extensionality Axiom}}% \label{ref:extensionality-axiom} @@ -236,6 +242,12 @@ Given \nameref{ref:relation} $R$, the \textbf{range} of $R$, denoted $\ran{R}$, \end{definition} +\section{\partial{Reflexive Relation}}% +\label{ref:reflexive-relation} + +A binary relation $R$ is \textbf{reflexive} on $A$ if and only if $xRx$ for all + $x \in A$. + \section{\defined{Relation}}% \label{ref:relation} @@ -272,6 +284,12 @@ For each formula $\phi$ not containing $B$, the following is an axiom: \end{axiom} +\section{\partial{Symmetric Relation}}% +\label{ref:symmetric-relation} + +A binary relation $R$ is \textbf{symmetric} on $A$ if and only if whenever + $xRy$ then $yRx$. + \section{\defined{Symmetric Difference}}% \label{ref:symmetric-difference} @@ -284,6 +302,12 @@ The \textbf{symmetric difference} $A + B$ of sets $A$ and $B$ is the set \end{definition} +\section{\partial{Transitive Relation}}% +\label{ref:transitive-relation} + +A binary relation $R$ is \textbf{transitive} on $A$ if and only if whenever + $xRy$ and $yRz$, then $xRz$. + \section{\defined{Union Axiom}}% \label{ref:union-axiom} @@ -3148,6 +3172,25 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \end{proof} +\section{Equivalence Relations}% +\label{sec:equivalence-relations} + +\subsection{\unverified{Theorem 3M}}% +\label{sub:theorem-3m} + +\begin{theorem}[3M] + + If $R$ is a symmetric and transitive relation, then $R$ is an equivalence + relation on $\fld{R}$. + +\end{theorem} + +\begin{proof} + + TODO + +\end{proof} + \section{Exercises 3}% \label{sec:exercises-3} diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean index 097a1b3..4e32725 100644 --- a/Bookshelf/Enderton/Set/Chapter_2.lean +++ b/Bookshelf/Enderton/Set/Chapter_2.lean @@ -1,9 +1,6 @@ -import Mathlib.Data.Set.Basic -import Mathlib.Data.Set.Lattice - import Bookshelf.Enderton.Set.Chapter_1 -import Common.Logic.Basic import Common.Set.Basic +import Mathlib.Data.Set.Lattice /-! # Enderton.Chapter_2 diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 3e18297..8e753d0 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -1,6 +1,6 @@ import Bookshelf.Enderton.Set.Chapter_2 -import Common.Set.OrderedPair -import Common.Set.Relation +import Bookshelf.Enderton.Set.OrderedPair +import Bookshelf.Enderton.Set.Relation /-! # Enderton.Chapter_3 diff --git a/Common/Set/OrderedPair.lean b/Bookshelf/Enderton/Set/OrderedPair.lean similarity index 100% rename from Common/Set/OrderedPair.lean rename to Bookshelf/Enderton/Set/OrderedPair.lean diff --git a/Common/Set/Relation.lean b/Bookshelf/Enderton/Set/Relation.lean similarity index 99% rename from Common/Set/Relation.lean rename to Bookshelf/Enderton/Set/Relation.lean index 9ca9452..1ed02d2 100644 --- a/Common/Set/Relation.lean +++ b/Bookshelf/Enderton/Set/Relation.lean @@ -1,6 +1,4 @@ -import Common.Set.OrderedPair -import Mathlib.Data.Set.Basic -import Mathlib.Data.Set.Prod +import Bookshelf.Enderton.Set.OrderedPair /-! # Relations diff --git a/Common/Set.lean b/Common/Set.lean index 76ba02f..ae92e76 100644 --- a/Common/Set.lean +++ b/Common/Set.lean @@ -1,5 +1,3 @@ import Common.Set.Basic import Common.Set.Interval -import Common.Set.OrderedPair -import Common.Set.Partition -import Common.Set.Relation \ No newline at end of file +import Common.Set.Partition \ No newline at end of file