From dd430d83794421421059007c848bf855cd96d1b5 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 13 Jul 2023 13:56:01 -0600 Subject: [PATCH] Enderton. Draft up ordering relation section. --- Bookshelf/Enderton/Set.tex | 134 ++++++++++++++++++++++++++++++++++++ Common.lean | 1 + Common/Algebra.lean | 1 + Common/Algebra/Classes.lean | 13 ++++ 4 files changed, 149 insertions(+) create mode 100644 Common/Algebra.lean create mode 100644 Common/Algebra/Classes.lean diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 9393eb7..9658f8d 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -87,6 +87,17 @@ The \textbf{composition} of sets $F$ and $G$ is \end{definition} +\section{\defined{Connected}}% +\hyperlabel{ref:connected} + +A binary relation $R$ on $A$ is \textbf{connected} if for distinct $x, y \in A$, either $xRy$ or $yRx$. + +\begin{definition} + + \lean*{Common/Algebra/Classes}{IsConnected} + +\end{definition} + \section{\defined{Domain}}% \hyperlabel{ref:domain} @@ -220,6 +231,36 @@ The \textbf{inverse} of a set $F$ is the set \end{definition} +\section{\defined{Irreflexive}}% +\hyperlabel{ref:irreflexive} + +A binary relation $R$ on set $A$ is \textbf{irreflexive} if there is no $x \in A$ for which $xRx$. + +\begin{definition} + + \lean*{Mathlib/Init/Algebra/Classes}{IsIrrefl} + +\end{definition} + +\section{\defined{Linear Ordering}} +\hyperlabel{ref:linear-ordering} + +Let $A$ be any set. +A \textbf{linear ordering} on $A$ (also called a \textbf{total ordering} on $A$) + is a binary relation $R$ on $A$ (i.e., $R \subseteq A \times A$) meeting the + following two conditions: + +\begin{enumerate}[(a)] + \item $R$ is \nameref{ref:transitive}. + \item $R$ is \nameref{ref:trichotomous}. +\end{enumerate} + +\begin{definition} + + \lean*{Mathlib/Init/Algebra/Classes}{IsLinearOrder} + +\end{definition} + \section{\defined{Ordered Pair}}% \hyperlabel{ref:ordered-pair} @@ -415,6 +456,20 @@ A binary relation $R$ is \textbf{transitive} if and only if whenever $xRy$ and \end{definition} +\section{\defined{Trichotomous}}% +\hyperlabel{ref:trichotomous} + +A binary relation $R$ on set $A$ is \textbf{trichotomous} if for any + $x, y \in A$, exactly one of the three alternatives + $$xRy, \quad x = y, \quad yRx$$ + holds. + +\begin{definition} + + \lean*{Mathlib/Init/Algebra/Classes}{IsTrichotomous} + +\end{definition} + \section{\defined{Union Axiom}}% \hyperlabel{ref:union-axiom} @@ -3498,6 +3553,42 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \end{proof} +\section{Ordering Relations}% +\hyperlabel{sec:ordering-relations} + +\subsection{\pending{Theorem 3R}}% +\hyperlabel{sub:theorem-3r} + +\begin{theorem}[3R] + + Let $R$ be a linear ordering on $A$. + \begin{enumerate}[(i)] + \item There is no $x$ for which $xRx$. + \item For distinct $x$ and $y$ in $A$, either $xRy$ or $yRx$. + \end{enumerate} + +\end{theorem} + +\begin{proof} + + Suppose $R$ is a \nameref{ref:linear-ordering} on $A$. + + \paragraph{(i)}% + + Let $x \in A$. + By definition, $R$ is \nameref{ref:trichotomous}. + Then only one of $xRx$ and $x = x$ can hold. + Since $x = x$ obviously holds, it follows $\pair{x, x} \not\in R$. + + \paragraph{(ii)}% + + Let $x, y \in A$ such that $x \neq y$. + By definition, $R$ is \nameref{ref:trichotomous}. + Thus only one of $$xRy, \quad x = y, \quad yRx$$ hold. + By hypothesis $x \neq y$ meaning either $xRy$ or $yRx$. + +\end{proof} + \section{Exercises 3}% \hyperlabel{sec:exercises-3} @@ -5454,4 +5545,47 @@ State precisely the "analogous results" mentioned in Theorem 3Q. \end{proof} +\subsection{\sorry{Exercise 3.43}}% +\label{sub:exercise-3.43} + +Assume that $R$ is a linear ordering on a set $A$. +Show that $R^{-1}$ is also a linear ordering on $A$. + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\sorry{Exercise 3.44}}% +\label{sub:exercise-3.44} + +Assume that $<$ is a linear orderinng on a set $A$. +Assume that $f \colon A \rightarrow A$ and that $f$ has the property that + whenever $x < y$, then $f(x) < f(y)$. +Show that $f$ is one-to-one and that whenever $f(x) < f(y)$, then $x < y$. + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\sorry{Exercise 3.45}}% +\label{sub:exercise-3.45} + +Assume that $<_A$ and $<_B$ are linear orderings on $A$ and $B$, respectively. +Define the binary relation $<_L$ on the Cartesian product $A \times B$ by: + $$\pair{a_1, b_1} <_L \pair{a_2, b_2} \quad\text{iff}\quad + \text{either } a_1 <_A a_2 \text{ or } (a_1 = a_2 \land b_1 <_B b_2).$$ +Show that $<_L$ is a linear ordering on $A \times B$. +(The relation $<_L$ is called \textit{lexicographic} ordering, being the + ordering used in making dictionaries.) + +\begin{proof} + + TODO + +\end{proof} + \end{document} diff --git a/Common.lean b/Common.lean index dc64440..39037ec 100644 --- a/Common.lean +++ b/Common.lean @@ -1,3 +1,4 @@ +import Common.Algebra import Common.Finset import Common.List import Common.Logic diff --git a/Common/Algebra.lean b/Common/Algebra.lean new file mode 100644 index 0000000..46d0ab1 --- /dev/null +++ b/Common/Algebra.lean @@ -0,0 +1 @@ +import Common.Algebra.Classes \ No newline at end of file diff --git a/Common/Algebra/Classes.lean b/Common/Algebra/Classes.lean new file mode 100644 index 0000000..21ef4c7 --- /dev/null +++ b/Common/Algebra/Classes.lean @@ -0,0 +1,13 @@ +import Mathlib.Init.Algebra.Classes + +/-! # Common.Algebra.Classes + +Additional theorems and definitions useful in the context of algebraic classes. +-/ + +/-- +`IsConnected X lt` means that the binary relation `lt` on `X` is connected, that +is, either `lt a b` or `lt b a` for any distinct `a` and `b`. +-/ +class IsConnected (α : Type u) (lt : α → α → Prop) : Prop where + connected : ∀ a b, a ≠ b → lt a b ∨ lt b a \ No newline at end of file