diff options
Diffstat (limited to 'library')
37 files changed, 5885 insertions, 0 deletions
diff --git a/library/algebra/group.tex b/library/algebra/group.tex new file mode 100644 index 0000000..48934bd --- /dev/null +++ b/library/algebra/group.tex @@ -0,0 +1 @@ +\section{Groups} diff --git a/library/algebra/loop.tex b/library/algebra/loop.tex new file mode 100644 index 0000000..338985c --- /dev/null +++ b/library/algebra/loop.tex @@ -0,0 +1,7 @@ +\import{algebra/quasigroup.tex} + +\section{Loops} + +\begin{struct}\label{loop} + A loop $A$ is a quasigroup and a unital magma. +\end{struct} diff --git a/library/algebra/magma.tex b/library/algebra/magma.tex new file mode 100644 index 0000000..6f5ac04 --- /dev/null +++ b/library/algebra/magma.tex @@ -0,0 +1,100 @@ +\import{function.tex} + +\section{Magmas} + +\begin{struct}\label{magma} + A magma $A$ is a onesorted structure equipped with + \begin{enumerate} + \item $\mul$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{magma_welldef} for all $a, b\in \carrier[A]$ we have $\mul[A](a,b)\in \carrier[A]$. + \end{enumerate} +\end{struct} + +\begin{abbreviation}\label{cdot} + $a\cdot b = \mul(a,b)$. +\end{abbreviation} + +\begin{abbreviation}\label{idempotentelement} + $a$ is an idempotent element of $A$ iff + $a\in\carrier[A]$ and + $\mul[A](a,a) = a$. +\end{abbreviation} + + +\begin{definition}\label{idempotents} + $\idempotents{A} = \{a\in\carrier[A]\mid \mul[A](a,a) = a\}$. +\end{definition} + +%\begin{definition}\label{rightinternalorbit} +% $\rightinternalorbit{a}{A} = \{\mul[A](a,a') \mid a'\in\carrier[A]\}$. +%\end{definition} + +\begin{abbreviation}\label{commutes} + $a$ commutes with $b$ iff $a\cdot b = b\cdot a$. +\end{abbreviation} + +\begin{definition}\label{submagma} + $A$ is a submagma of $B$ iff + $A$ is a magma and + $B$ is a magma and + $\carrier[A]\subseteq \carrier[B]$ and + $\mul[A]\subseteq \mul[B]$. +\end{definition} + +\begin{proposition}\label{submagma_transitive} + Suppose $A$ is a submagma of $B$. + Suppose $B$ is a submagma of $C$. + Then $A$ is a submagma of $C$. +\end{proposition} +\begin{proof} + Follows by \cref{submagma,subseteq_transitive}. +\end{proof} + +\begin{struct}\label{unitalmagma} + A unital magma $A$ is a magma equipped with + \begin{enumerate} + \item $\neutral$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{unitalmagma_type} $\neutral[A]\in \carrier[A]$. + \item\label{unitalmagma_right} for all $a\in \carrier[A]$ we have $\mul[A](a,\neutral[A]) = a$. + \item\label{unitalmagma_left} for all $a\in \carrier[A]$ we have $\mul[A](\neutral[A], a) = a$. + \end{enumerate} +\end{struct} + +\begin{proposition}\label{unitalmagma_mul_neutral_neutral} + Let $A$ be a unital magma. + Then $\mul(\neutral,\neutral) = \neutral$. +\end{proposition} + +\begin{proposition}\label{unitalmagma_neutral_unique} + Let $A$ be a unital magma. + Let $e$ be a set such that $e\in A$ and for all $x\in A$ we have $\mul(x, e) = x = \mul(e, x)$. + Then $e = \neutral$. +\end{proposition} +\begin{proof} + Follows by \cref{unitalmagma_type,unitalmagma_left}. +\end{proof} + + + +\begin{definition}[Left orbit]\label{left_orbit} + $\LeftOrb{x}{A} = \{\mul[A](a,x) \mid a\in\carrier[A] \}$. +\end{definition} + +\begin{proposition}\label{eq_left_orbit_witness} + Let $A$ be a magma. + Let $e,f\in\carrier[A]$. + Suppose $\LeftOrb{e}{A} = \LeftOrb{f}{A}$. + Let $x\in\carrier[A]$. + Then there exists $y\in\carrier[A]$ such that $x\cdot e = y\cdot f$. +\end{proposition} +\begin{proof} + We have $x\cdot e\in \LeftOrb{e}{A}$ by \cref{left_orbit}. + Thus $x\cdot e\in\LeftOrb{f}{A}$ by assumption. + Take $y\in\carrier[A]$ such that $x\cdot e = y\cdot f$ by \cref{left_orbit}. +\end{proof} diff --git a/library/algebra/quasigroup.tex b/library/algebra/quasigroup.tex new file mode 100644 index 0000000..747ab03 --- /dev/null +++ b/library/algebra/quasigroup.tex @@ -0,0 +1,36 @@ +\import{algebra/magma.tex} + +\section{Quasigroups} + +\begin{struct}\label{quasigroup} + A quasigroup $A$ is a magma equipped with + \begin{enumerate} + \item $\ldiv$ + \item $\rdiv$ + \end{enumerate} + such that + \begin{enumerate} + \item for all $a, b\in A$ we have $\ldiv (a,b)\in A$. + \item for all $a, b\in A$ we have $\rdiv (a,b)\in A$. + \item for all $a,b \in A$ we have $b = \mul(a,\ldiv (a,b))$. + \item for all $a,b \in A$ we have $b = \ldiv(a,\mul (a,b))$. + \item for all $a,b \in A$ we have $b = \mul(\rdiv (b,a),a)$. + \item for all $a,b \in A$ we have $b = \rdiv(\mul (b,a),a)$. + \end{enumerate} +\end{struct} + +% Cancelling an element on the left. +\begin{lemma}\label{quasigroup_cancel_left} + Let $A$ be a quasigroup. + Let $a,b,c \in A$. + Suppose $\mul(a,b) = \mul(a,c)$. + Then $b = c$. +\end{lemma} + +% Cancelling an element on the right. +\begin{lemma}\label{quasigroup_cancel_right} + Let $A$ be a quasigroup. + Let $a,b,c \in A$. + Suppose $\mul(a,c) = \mul(b,c)$. + Then $a = b$. +\end{lemma} diff --git a/library/algebra/semigroup.tex b/library/algebra/semigroup.tex new file mode 100644 index 0000000..e090a56 --- /dev/null +++ b/library/algebra/semigroup.tex @@ -0,0 +1,82 @@ +\import{algebra/magma.tex} + +\section{Semigroups} + +\begin{struct}\label{semigroup} + A semigroup $A$ is a magma such that + \begin{enumerate} + %\item for all $a, b, c\in \carrier[A]$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. + \item\label{semigroup_assoc} for all $a, b, c$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. + \end{enumerate} +\end{struct} + + + +\section{Regular semigroups} + + +\begin{struct}\label{regularsemigroup} + A regular semigroup $A$ is a semigroup such that + \begin{enumerate} + %\item for all $a\in \carrier[A]$ there exists $b\in\carrier[A]$ such that $\mul[A](a, \mul[A](b, a)) = a$. + \item\label{regularsemigroup_regular} for all $a$ there exists $b\in\carrier[A]$ such that $\mul[A](a, \mul[A](b, a)) = a$. + \end{enumerate} +\end{struct} + + + +\section{Inverse semigroups} + +\begin{struct}\label{inversesemigroup} + An inverse semigroup $A$ is a regular semigroup such that + \begin{enumerate} + \item\label{inversesemigroup_comm} for all $a,b\in\idempotents{A}$ we have $\mul[A](a, b) = \mul[A](b, a)$. + \end{enumerate} +\end{struct} + +\begin{proposition}\label{inversesemigroup_is_semigroup} + Suppose $A$ is an inverse semigroup. + Then $A$ is a semigroup. +\end{proposition} + + +\begin{proposition}\label{inversesemigroup_is_regularsemigroup} + Suppose $A$ is an inverse semigroup. + Then $A$ is a regular semigroup. +\end{proposition} + +\begin{proposition}\label{idempotentelems_eq_iff_orbits_eq} + Let $A$ be an inverse semigroup. + Let $e,f\in\idempotents{A}$. + % TODO use Orbits explicitly? + Suppose for all $x\in\carrier[A]$ there exists $y\in\carrier[A]$ + such that $x\cdot e = y\cdot f$. + Suppose for all $x\in\carrier[A]$ there exists $y\in\carrier[A]$ + such that $x\cdot f = y\cdot e$. + Then $e = f$. +\end{proposition} +\begin{proof} + Take $x, y\in\carrier[A]$ such that $e = x\cdot f$ and $f = y\cdot e$ by \cref{idempotents}. + % + \begin{align*} + e + &= x \cdot f + \explanation{by assumption}\\ + &= x\cdot (f\cdot f) + \explanation{by \cref{idempotents}}\\ + &= (x\cdot f)\cdot f + \explanation{by \cref{semigroup_assoc,inversesemigroup_is_semigroup}}\\ + &= e\cdot f + \explanation{by assumption}\\ + &= f\cdot e + \explanation{by \hyperref[inversesemigroup_comm]{commutativity of idempotent elements}}\\ + &= (y\cdot e)\cdot e + \explanation{by assumption}\\ + &= y\cdot (e\cdot e) + \explanation{by \cref{semigroup_assoc,inversesemigroup_is_semigroup}}\\ + &= y \cdot e + \explanation{by \cref{idempotents}}\\ + &= f + \explanation{by assumption} + \end{align*} +\end{proof} diff --git a/library/cardinal.tex b/library/cardinal.tex new file mode 100644 index 0000000..d0dec59 --- /dev/null +++ b/library/cardinal.tex @@ -0,0 +1,14 @@ +\section{Cardinality} + +\import{set.tex} +\import{ordinal.tex} +\import{function.tex} + +\begin{definition}\label{finite} + $X$ is finite iff there exists a natural number $k$ such that + there exists a bijection from $k$ to $X$. +\end{definition} + +\begin{abbreviation}\label{infinite} + $X$ is infinite iff $X$ is not finite. +\end{abbreviation} diff --git a/library/everything.tex b/library/everything.tex new file mode 100644 index 0000000..9b85f83 --- /dev/null +++ b/library/everything.tex @@ -0,0 +1,32 @@ +\import{set.tex} +\import{set/cons.tex} +\import{set/symdiff.tex} +\import{set/product.tex} +\import{set/powerset.tex} +\import{set/bipartition.tex} +\import{set/partition.tex} +\import{set/cantor.tex} +\import{set/filter.tex} +\import{set/fixpoint.tex} +\import{relation.tex} +\import{relation/properties.tex} +\import{order/quasiorder.tex} +\import{relation/equivalence.tex} +\import{relation/closure.tex} +\import{relation/uniqueness.tex} +\import{function.tex} +\import{ordinal.tex} +%\import{nat.tex} +\import{cardinal.tex} +\import{algebra/magma.tex} +\import{algebra/semigroup.tex} +\import{order/order.tex} +%\import{order/semilattice.tex} +\import{topology/topological-space.tex} +\import{topology/basis.tex} +\import{topology/disconnection.tex} +\import{topology/separation.tex} + +\begin{proposition}\label{trivial} + $x = x$. +\end{proposition} diff --git a/library/function.tex b/library/function.tex new file mode 100644 index 0000000..eb64de2 --- /dev/null +++ b/library/function.tex @@ -0,0 +1,753 @@ +\section{Functions} + +\import{set.tex} +\import{relation.tex} +\import{relation/uniqueness.tex} + + +\begin{abbreviation}\label{function} + $f$ is a function iff $f$ is right-unique and $f$ is a relation. +\end{abbreviation} + +% The builtin "-(-)" notation desugars to "\apply{-}{-}". +\begin{definition}\label{apply} + $\apply{f}{x} = \unions{\img{f}{\{x\}}}$. +\end{definition} + +\begin{proposition}\label{function_rightunique} + Let $f$ be a function. + Suppose $(a,b), (a, b')\in f$. + Then $b = b'$. +\end{proposition} +\begin{proof} + Follows by \hyperref[rightunique]{right-uniqueness}. +\end{proof} + +\begin{proposition}\label{function_apply_intro} + Let $f$ be a function. + Suppose $(a,b)\in f$. + Then $f(a) = b$. +\end{proposition} +\begin{proof} + Let $B = \img{f}{\{a\}}$. + $B = \{b'\in\ran{f}\mid (a,b')\in f \}$ by \cref{img_singleton}. + $b\in\ran{f}$. + For all $b'\in B$ we have $(a, b')\in f$. + For all $b', b''\in B$ we have $b' = b''$ by \hyperref[rightunique]{right-uniqueness}. + Then $B = \{b\}$ by \cref{singleton_iff_inhabited_subsingleton}. + Then $\unions{B} = b$. + Thus $f(a) = b$ by \cref{apply}. +\end{proof} + +\begin{proposition}\label{function_member_elim} + Let $f$ be a function. + Suppose $w\in f$. + Then there exists $x\in\dom{f}$ such that $w = (x, f(x))$. +\end{proposition} +\begin{proof} + Follows by \cref{apply,function_apply_intro,dom,relation}. +\end{proof} + +\begin{proposition}\label{function_apply_elim} + Let $f$ be a function. + Suppose $x\in\dom{f}$. + Then $(x,f(x))\in f$. +\end{proposition} +\begin{proof} + Follows by \cref{dom_iff,function_apply_intro}. +\end{proof} + +\begin{proposition}\label{function_apply_iff} + Let $f$ be a function. + $(a,b)\in f$ iff $a\in\dom{f}$ and $f(a) = b$. +\end{proposition} + +\begin{proposition}\label{fun_subseteq} + Let $f, g$ be functions. + Suppose $\dom{f}\subseteq \dom{g}$. + Suppose for all $x\in\dom{f}$ we have $f(x) = g(x)$. + Then $f\subseteq g$. +\end{proposition} +\begin{proof} + For all $x,y$ such that $(x,y)\in f$ we have $(x,y)\in g$. + Follows by \cref{subseteq,relation}. +\end{proof} + +\begin{proposition}[Function extensionality]\label{funext} + Let $f, g$ be functions. + Suppose $\dom{f} = \dom{g}$. + Suppose for all $x$ we have $f(x) = g(x)$. + Then $f = g$. +\end{proposition} +\begin{proof} + $\dom{f}\subseteq \dom{g}\subseteq \dom{f}$. + For all $x\in\dom{f}$ we have $f(x) = g(x)$. + Thus $f\subseteq g$. + For all $x\in\dom{g}$ we have $f(x) = g(x)$. + Thus $g\subseteq f$. +\end{proof} + +\begin{proposition}\label{fun_ran_iff} + Let $f$ be a function. + $b\in\ran{f}$ iff there exists $a\in\dom{f}$ such that $f(a) = b$. +\end{proposition} +\begin{proof} + Follows by \cref{ran,function_apply_iff}. +\end{proof} + +\begin{abbreviation}\label{function_on} + $f$ is a function on $X$ iff $f$ is a function and $X = \dom{f}$. +\end{abbreviation} + +\begin{abbreviation}\label{function_to} + $f$ is a function to $Y$ iff $f$ is a function and for all $x\in\dom{f}$ we have $f(x)\in Y$. +\end{abbreviation} + +\begin{proposition}\label{function_on_weaken_codom} + Let $f$ be a function to $B$. + Suppose $B\subseteq C$. + Then $f$ is a function to $C$. +\end{proposition} + +\begin{proposition}\label{function_to_ran} + Let $f$ be a function to $B$. + Then $\ran{f}\subseteq B$. +\end{proposition} +\begin{proof} + Follows by \cref{ran,subseteq,apply,function_member_elim,pair_eq_iff,dom}. +\end{proof} + +\begin{definition}\label{funs} + $\funs{A}{B} = \{ f\in\rels{A}{B}\mid \text{$A = \dom{f}$ and $f$ is right-unique}\}$. +\end{definition} + +\begin{abbreviation}\label{function_from_to} + $f$ is a function from $X$ to $Y$ iff $f\in\funs{X}{Y}$. +\end{abbreviation} + +\begin{proposition}\label{funs_is_relation} + Let $f\in\funs{A}{B}$. + Then $f$ is a relation. +\end{proposition} +\begin{proof} + Follows by \cref{funs,rels_is_relation}. +\end{proof} + +\begin{proposition}\label{funs_is_function} + Let $f\in\funs{A}{B}$. + Then $f$ is a function. +\end{proposition} + +\begin{proposition}\label{funs_subseteq_rels} + $\funs{A}{B}\subseteq\rels{A}{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{funs,subseteq}. +\end{proof} + +\begin{proposition}\label{funs_intro} + Let $f$ be a function to $B$ such that $A=\dom{f}$. + Then $f\in\funs{A}{B}$. +\end{proposition} +\begin{proof} + %$f$ is a function. + $\dom{f}\subseteq A$ by \cref{subseteq_refl}. + $\ran{f}\subseteq B$ by \cref{function_to_ran}. + Thus $f\in\rels{A}{B}$ by \cref{rels_intro_dom_and_ran}. + Thus $f\in\funs{A}{B}$ by \cref{funs}. +\end{proof} + +\begin{proposition}\label{funs_elim} + Let $f\in\funs{A}{B}$. + Then $f$ is a function to $B$ such that $A = \dom{f}$. +\end{proposition} +\begin{proof} + $f$ is a function by \cref{funs_is_function}. % and in particular, a relation. + It suffices to show that for all $a\in\dom{f}$ we have $f(a)\in B$ by \cref{funs}. + Fix $a\in\dom{f}$. + Take $b$ such that $f(a) = b$. + Thus $(a,b)\in f$ by \cref{function_apply_elim}. + Now $b\in\ran{f}$ by \cref{ran_iff}. + Finally $\ran{f}\subseteq B$ by \cref{funs,rels_ran_subseteq}. +\end{proof} + +\begin{proposition}\label{funs_weaken_codom} + Let $f\in\funs{A}{B}$. + Suppose $B\subseteq D$. + Then $f\in\funs{A}{D}$. +\end{proposition} +\begin{proof} + $f\in\rels{A}{D}$ by \cref{funs,rels_weaken_codom}. + Follows by \cref{funs}. +\end{proof} + +\begin{proposition}\label{funs_type_apply} + Let $f\in\funs{A}{B}$. + Let $a\in A$. + Then $f(a)\in B$. +\end{proposition} +\begin{proof} + $(a,f(a)) \in f$ by \cref{funs_elim,function_apply_iff}. + Thus $f(a)\in B$ by \cref{funs,rels_type_ran}. +\end{proof} + +\begin{proposition}\label{funs_tuple_intro} + Let $f\in\funs{A}{B}$. + Let $a\in A$. + Then there exists $b\in B$ such that $(a,b)\in f$. +\end{proposition} +\begin{proof} + $(a,f(a)) \in f$ by \cref{funs_elim,function_apply_iff}. + $f(a)\in B$ by \cref{funs_type_apply}. +\end{proof} + + +% LATER techincally ambiguous with the current grammar (as of 2022-04-24) +% but the ambiguity gets resolved during interpretation. +% the options are (probably): +% +% 1: function such that ( ... and for all ...) +% 2: (function such that ...) and for all +% +% \begin{definition} +% $f$ is a function from $X$ to $Y$ iff $f$ is a function such that $\dom{f} = X$ and for all $x\in X$ we have $f(x)\in Y$. +% \end{definition} + +\begin{proposition}\label{funs_ran} + Let $f\in\funs{A}{B}$. + Then $\ran{f}\subseteq B$. +\end{proposition} +\begin{proof} + $f$ is a function to $B$. +\end{proof} + + + +\subsection{Image of a function} + +\begin{proposition}\label{img_of_function_intro} + Let $f$ be a function. + Suppose $x\in\dom{f}\inter X$. + Then $f(x)\in \img{f}{X}$. +\end{proposition} +\begin{proof} + $x\in X$ by \cref{inter_elim_right}. + Thus $(x,f(x))\in f$ by \cref{function_apply_elim,inter_elim_left}. +\end{proof} + +\begin{proposition}\label{img_of_function_elim} + Let $f$ be a function. + Suppose $y\in \img{f}{X}$. + Then there exists $x\in\dom{f}\inter X$ such that $y = f(x)$. +\end{proposition} +\begin{proof} + Take $x\in X$ such that $(x,y)\in f$. + Then $x\in\dom{f}$ and $y = f(x)$ by \cref{dom_intro,function_apply_iff}. +\end{proof} + +\begin{proposition}\label{img_of_function} + Suppose $f$ is a function. + $\img{f}{X} = \{ f(x) \mid x\in\dom{f}\inter X\}$. +\end{proposition} +\begin{proof} + Follows by \cref{img_of_function_intro,img_of_function_elim}. +\end{proof} + +\subsection{Families of functions} + +\begin{abbreviation}\label{family_of_functions} + $F$ is a family of functions iff + every element of $F$ is a function. +\end{abbreviation} + +\begin{proposition}\label{unions_of_compatible_family_of_function_is_function} + Let $F$ be a family of functions. + Suppose that for all $f,g \in F$ we have $f\subseteq g$ or $g\subseteq f$. + Then $\unions{F}$ is a function. +\end{proposition} +\begin{proof} + $\unions{F}$ is a relation by \cref{unions_of_family_of_relations_is_relation}. + For all $x,y, y'$ such that $(x,y),(x,y')\in \unions{F}$ + there exists $f\in F$ such that $(x,y),(x,y')\in f$ + by \cref{unions_iff,subseteq}. + %Hence for all $x,y, y'$ such that $(x,y),(x,y')\in \unions{F}$ we have $y = y'$ + % by \cref{rightunique}. + Thus $\unions{F}$ is right-unique by \cref{rightunique}. +\end{proof} + + +\subsection{The empty function} + +\begin{proposition}\label{emptyset_is_function} + $\emptyset$ is a function. +\end{proposition} +%\begin{proof} +% For all $x,y, y'$ we have +% if $(x,y),(x,y')\in \emptyset$, then $y = y'$. +%\end{proof} + +\begin{proposition}\label{emptyset_is_function_on_emptyset} + $\emptyset$ is a function on $\emptyset$. +\end{proposition} + +\begin{proposition}\label{codom_of_emptyset_can_be_anything} + $\emptyset$ is a function to $X$. +\end{proposition} + +\begin{proposition}\label{emptyset_is_injective} + $\emptyset$ is injective. +\end{proposition} +% LATER filter throws out the definition of injective, smh + + +\subsection{Function composition} + +\begin{abbreviation}\label{composable} + $g$ is composable with $f$ iff $\ran{f}\subseteq \dom{g}$. +\end{abbreviation} + +\begin{proposition}\label{function_circ} + Suppose $f$ and $g$ are right-unique. + Then $g\circ f$ is a function. +\end{proposition} + +\begin{proposition}\label{circ_apply} + Let $f, g$ be functions. + Suppose $g$ is composable with $f$. + Let $x\in\dom{f}$. + Then $(g\circ f)(x) = g(f(x))$. +\end{proposition} +\begin{proof} + $(x, g(f(x)))\in g\circ f$ by \cref{circ,ran,subseteq,function_apply_elim}. + $g\circ f$ is a function by \cref{function_circ}. + Thus $(g\circ f)(x) = g(f(x))$ by \cref{function_apply_intro}. +\end{proof} + +\begin{proposition}\label{dom_of_circ} + Let $f, g$ be functions. + Suppose $g$ is composable with $f$. + $\dom{g\circ f} = \preimg{f}{\dom{g}}$. +\end{proposition} +\begin{proof} + Every element of $\dom{g\circ f}$ is an element of $\preimg{f}{\dom{g}}$ + by \cref{preimg,circ,dom,pair_eq_iff}. + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{dom_circ_exact} + Let $f, g$ be functions. + Suppose $\ran{f} = \dom{g}$. + $\dom{g\circ f} = \dom{f}$. +\end{proposition} +\begin{proof} + Every element of $\dom{g\circ f}$ is an element of $\dom{f}$. + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{ran_of_circ_intro} + Let $f, g$ be functions. + Suppose $g$ is composable with $f$. + Suppose $y\in \img{g}{\ran{f}}$. + Then $y\in \ran{g\circ f}$. +\end{proposition} +\begin{proof} + Take $x\in\ran{f}$ such that $(x, y)\in g$. + Take $x'\in\dom{f}$ such that $(x', x)\in f$. + Then $(x', y) \in g\circ f$. + Follows by \cref{ran_intro}. +\end{proof} + +\begin{proposition}\label{ran_of_circ_elim} + Let $f, g$ be functions. + Suppose $g$ is composable with $f$. + Suppose $y\in \ran{g\circ f}$. + Then $y\in \img{g}{\ran{f}}$. +\end{proposition} +\begin{proof} + Take $x\in\dom{f}$ such that $(x, y)\in g\circ f$ + by \cref{circ,circ_iff,ran,dom}. + $f(x)\in\ran{f}$. + $(f(x), y)\in g$ + by \cref{function_apply_intro,apply,circ_iff}. + Follows by \cref{img_iff}. +\end{proof} + +\begin{proposition}\label{ran_of_circ} + Let $f, g$ be functions. + Suppose $g$ is composable with $f$. + Then $\ran{g\circ f} = \img{g}{\ran{f}}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{ran_circ_exact} + Let $f, g$ be functions. + Suppose $\ran{f} = \dom{g}$. + Then $\ran{g\circ f} = \ran{g}$. +\end{proposition} +\begin{proof} + \begin{align*} + \ran{g\circ f} + &= \img{g}{\ran{f}} + \explanation{by \cref{subseteq_refl,ran_of_circ}}\\ + &= \img{g}{\dom{g}} + \\ % by assumption + &= \ran{g} + \explanation{by \cref{img_dom}} + \end{align*} +\end{proof} + + +\begin{proposition}\label{img_of_circ_elim} + Let $f, g$ be functions. + Let $A$ be a set. + Suppose $\ran{f}\subseteq \dom{g}$. + Suppose $c\in\img{g\circ f}{A}$. + Then $c\in\img{g}{\img{f}{A}}$. +\end{proposition} +\begin{proof} + Take $a\in A$ such that $(a,c)\in g\circ f$. + Take $b$ such that $(a,b)\in f$ and $(b, c)\in g$. + Then $b\in\img{f}{A}$. + Follows by \cref{img_iff}. +\end{proof} + +\begin{proposition}\label{img_of_circ} + Let $f, g$ be functions. + Let $A$ be a set. + Suppose $\ran{f}\subseteq\dom{g}$. + Then $\img{g\circ f}{A} = \img{g}{\img{f}{A}}$. +\end{proposition} +\begin{proof} + For all $c$ we have $c\in\img{g}{\img{f}{A}}$ + iff $c\in\img{g\circ f}{A}$ + by \cref{circ_iff,img_iff}. + Follows by \hyperref[setext]{extensionality}. +\end{proof} + +\begin{proposition}\label{restrl_of_function_is_function} + Let $f$ be a function. + Let $A$ be a set. + $\restrl{f}{A}$ is a function. +\end{proposition} + +\begin{proposition}\label{restrl_of_function_apply} + Let $f$ be a function. + Suppose $A\subseteq\dom{f}$. + Let $a\in A$. + Then $(\restrl{f}{A})(a) = f(a)$. +\end{proposition} +\begin{proof} + Then $(a,f(a))\in f$. + Then $(a,f(a))\in \restrl{f}{A}$ by \cref{restrl_iff}. + Thus $(\restrl{f}{A})(a) = f(a)$. +\end{proof} + +\begin{proposition}\label{function_apply_default} + Suppose $x\notin\dom{f}$. + Then $f(x) = \emptyset$. +\end{proposition} +\begin{proof} + $\img{f}{\{x\}} = \emptyset$ by \cref{setext,notin_emptyset,img_singleton_iff,dom_intro}. + Follows by \cref{apply,unions_emptyset}. +\end{proof} + + + +\subsection{Injections} + +\begin{proposition}\label{injective_function} + Suppose $f$ is a function. + $f$ is injective iff for all $x,y\in\dom{f}$ we have $f(x) = f(y) \implies x = y$. +\end{proposition} +\begin{proof} + Follows by \cref{injective,function_apply_iff}. +\end{proof} + +\begin{abbreviation}\label{injection} + $f$ is an injection iff $f$ is an injective function. +\end{abbreviation} + +\begin{definition}\label{inj} + $\inj{A}{B} = \{f\in\funs{A}{B}\mid \text{for all $x,y\in A$ such that $f(x)=f(y)$ we have $x = y$}\}$. +\end{definition} + +\subsection{Surjections} + +\begin{abbreviation}\label{surjection} + $f$ is a surjection onto $Y$ iff $f$ is a function such that $f$ is surjective on $Y$. +\end{abbreviation} + +\begin{definition}\label{surj} + $\surj{A}{B} = \{f\in\funs{A}{B}\mid \text{for all $b\in B$ there exists $a\in A$ such that $f(a) = b$}\}$. +\end{definition} + +\begin{abbreviation}\label{surjection_from_to} + $f$ is a surjection from $A$ to $B$ iff $f\in\surj{A}{B}$. +\end{abbreviation} + +\begin{lemma}\label{surjection_ran} + Let $f$ be a function. + Then $f$ is surjective on $\ran{f}$. +\end{lemma} +\begin{proof} + It suffices to show that for all $y\in\ran{f}$ there exists $x\in\dom{f}$ such that $f(x) = y$. + Fix $y\in\ran{f}$. + Take $x$ such that $(x,y)\in f$. + Then $x\in\dom{f}$ and $f(x) = y$ by \cref{dom,function_apply_iff}. +\end{proof} + +\begin{lemma}\label{surj_to_fun} + Let $f\in\surj{A}{B}$. + Then $f\in\funs{A}{B}$. +\end{lemma} + +\begin{lemma}\label{fun_to_surj} + Let $f\in\funs{A}{B}$. + Then $f\in\surj{A}{\ran{f}}$. +\end{lemma} +\begin{proof} + $f\in\rels{A}{\ran{f}}$ by \cref{funs,rels_restrict_ran}. + Thus $f\in\funs{A}{\ran{f}}$ by \cref{funs}. + It suffices to show that for all $b\in\ran{f}$ there exists $a\in A$ such that $f(a) = b$ by \cref{surj}. + Fix $b\in\ran{f}$. + Take $a$ such that $(a,b)\in f$. + Thus $f(a)=b$ by \cref{function_apply_iff,funs_elim}. + We have $a\in\dom{f} = A$. + Follows by assumption. +\end{proof} + +\begin{corollary}\label{ran_of_surj} + Let $f\in\surj{A}{B}$. + Then $\ran{f} = B$. +\end{corollary} +\begin{proof} + % TODO clean + We have $f$ is a function by \cref{surj,funs_is_function}. + Now $\ran{f}\subseteq B$ by \cref{surj,funs_ran}. + It suffices to show that every element of $B$ is an element of $\ran{f}$. + It suffices to show that for all $b\in B$ + there exists $a\in\dom{f}$ such that $f(a) = b$ by \cref{fun_ran_iff}. + Fix $b\in B$. + Take $a\in A$ such that $f(a) = b$ by \cref{surj}. + Then $\dom{f} = A$ by \cref{surj,funs_elim}. +\end{proof} + +\begin{corollary}\label{funs_surj_iff} + Let $f\in\funs{A}{B}$. + Then $f\in\surj{A}{B}$ iff $\ran{f} = B$. +\end{corollary} +\begin{proof} + Follows by \cref{surj,fun_to_surj,ran_of_surj}. +\end{proof} + +\begin{proposition}\label{surjections_circ} + Let $f\in\surj{A}{B}$. + Let $g\in\surj{B}{C}$. + Then $g\circ f\in\surj{A}{C}$. +\end{proposition} +\begin{proof} + $\dom{f} = A$ by \cref{surj,funs}. + $\dom{g} = B = \ran{f}$ by \cref{surj,funs,ran_of_surj}. + $\dom{g\circ f} = A$ by \cref{surj_to_fun,funs_is_function,dom_circ_exact}. + Omitted. % TODO +\end{proof} + + + +\subsection{Bijections} + +\begin{definition}\label{bijections} + $\bijections{A}{B} = \{ f\in\surj{A}{B} \mid \text{$f$ is injective}\}$. +\end{definition} + +\begin{abbreviation}\label{bijection} + $f$ is a bijection from $A$ to $B$ iff $f\in\bijections{A}{B}$. +\end{abbreviation} + +\begin{proposition}\label{bijections_to_funs} + Every element of $\bijections{A}{B}$ is an element of $\funs{A}{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{bijections,surj}. +\end{proof} + +\begin{proposition}\label{bijection_is_function} + Every element of $\bijections{A}{B}$ is a function. +\end{proposition} +\begin{proof} + Follows by \cref{bijections_to_funs,funs_is_function}. +\end{proof} + +\begin{proposition}\label{bijections_dom} + Let $f\in\bijections{A}{B}$. + Then $\dom{f} = A$. +\end{proposition} +\begin{proof} + $f\in\funs{A}{B}$ by \cref{bijections_to_funs}. + Follows by \cref{funs}. +\end{proof} + +\begin{proposition}\label{bijection_circ} + Let $f$ be a bijection from $A$ to $B$. + Let $g$ be a bijection from $B$ to $C$. + Then $g\circ f$ is a bijection from $A$ to $C$. +\end{proposition} +\begin{proof} + $g\circ f\in\surj{A}{C}$ by \cref{bijections,surjections_circ}. + $g\circ f$ is an injection. +\end{proof} + +\subsection{Converse as a function} + +\begin{proposition}\label{converse_of_function_is_injective} + Let $f$ be a function. + Then $\converse{f}$ is injective. % i.e. an injective relation. +\end{proposition} + +\begin{proposition}\label{injective_converse_is_function} + Suppose $f$ is injective. % NOTE: f need not be a function! + Then $\converse{f}$ is a function. +\end{proposition} + +\begin{proposition}\label{bijective_converse_is_function} + Let $f$ be a bijection from $A$ to $B$. + Then $\converse{f}$ is a function. +\end{proposition} +\begin{proof} + Follows by \cref{bijections,injective_converse_is_function}. +\end{proof} + +\begin{proposition}\label{bijective_converse_are_funs} + Let $f$ be a bijection from $A$ to $B$. + Then $\converse{f}\in\funs{B}{A}$. +\end{proposition} +\begin{proof} + %\begin{align*} + % \dom{\converse{f}} + % &= \ran{f} + % \explanation{by \cref{dom_converse}}\\ + % &= B + % \explanation{by \cref{ran_of_surj}} + %\end{align*} + $\dom{\converse{f}} = \ran{f} = B$ by \cref{bijections,dom_converse,ran_of_surj}. + Omitted. % TODO +\end{proof} + +\begin{proposition}\label{bijective_converse_are_surjs} + Let $f$ be a bijection from $A$ to $B$. + Then $\converse{f}\in\surj{B}{A}$. +\end{proposition} +\begin{proof} + We have $\converse{f}\in\funs{B}{A}$ by \cref{bijective_converse_are_funs}. + It suffices to show that $\ran{\converse{f}} = A$ by \cref{funs_surj_iff}. + We have $\dom{f} = A$ by \cref{bijections_dom}. + Thus $\ran{\converse{f}} = A$ by \cref{ran_converse}. +\end{proof} + +\begin{proposition}\label{bijection_converse_is_bijection} + Let $f$ be a bijection from $A$ to $B$. + Then $\converse{f}$ is a bijection from $B$ to $A$. +\end{proposition} +\begin{proof} + $\converse{f}\in\funs{B}{A}$ by \cref{bijective_converse_are_funs}. + $\converse{f}$ is injective by \cref{bijection_is_function,converse_of_function_is_injective}. + $\converse{f}\in\surj{B}{A}$ by \cref{bijective_converse_are_surjs}. + Follows by \cref{bijections}. +\end{proof} + +\subsubsection{Inverses of a function} + +\begin{abbreviation}\label{leftinverse} + $g$ is a left inverse of $f$ iff for all $x\in\dom{f}$ we have $g(f(x)) = x$. +\end{abbreviation} + +% This definition of right inverse is probably not particularly useful... +\begin{abbreviation}\label{rightinverse} + $g$ is a right inverse of $f$ iff $f\circ g = \identity{\dom{g}}$. +\end{abbreviation} + +\begin{abbreviation}\label{rightinverseon} + $g$ is a right inverse of $f$ on $B$ iff $f\circ g = \identity{B}$. +\end{abbreviation} + +\begin{proposition}\label{injective_converse_is_leftinverse} + Let $f$ be an injection. + Then $\converse{f}$ is a left inverse of $f$. +\end{proposition} +\begin{proof} + $\converse{f}$ is a function by \cref{injective_converse_is_function}. + + Omitted. % TODO +\end{proof} + + + +\subsection{Identity function} + +\begin{proposition}\label{id_rightunique} + $\identity{A}$ is right-unique. +\end{proposition} +\begin{proof} + Follows by \cref{id,rightunique,pair_eq_iff}. +\end{proof} + +\begin{proposition}\label{id_is_function} + $\identity{A}$ is a function. +\end{proposition} + +\begin{proposition}\label{id_is_function_on} + $\identity{A}$ is a function on $A$. +\end{proposition} + +\begin{proposition}\label{id_is_function_to} + $\identity{A}$ is a function to $A$. +\end{proposition} + +\begin{proposition}\label{id_is_function_from_to} + $\identity{A}$ is a function from $A$ to $A$. +\end{proposition} +\begin{proof} + $\identity{A}\in\rels{A}{A}$ by \cref{id_elem_rels}. + Follows by \cref{funs,id_is_function_on,id_is_function_to}. +\end{proof} + +\begin{proposition}\label{id_apply} + Suppose $a\in A$. + % TODO/FIXME fix grammar, then simplify + %Then $\identity{A}(a) = a$. + Suppose $f = \identity{A}$. + Then $f(a) = a$. +\end{proposition} +\begin{proof} + $(a,a)\in\identity{A}$ by \cref{id_iff}. + Follows by \cref{id_is_function,function_apply_intro}. +\end{proof} + +\begin{proposition}\label{id_elem_funs} + $\identity{A}\in\funs{A}{A}$. +\end{proposition} +\begin{proof} + $\identity{A}$ is a function. + $\identity{A}\in\rels{A}{A}$. + $\dom{\identity{A}}\subseteq A$. +\end{proof} + + +\begin{proposition}\label{id_elem_surjections} + $\identity{A}\in\surj{A}{A}$. +\end{proposition} +\begin{proof} + We have $\identity{A}\in\funs{A}{A}$ by \cref{id_elem_funs}. + Omitted. % TODO +\end{proof} + +\begin{proposition}\label{id_elem_bijections} + $\identity{A}\in\bijections{A}{A}$. +\end{proposition} +\begin{proof} + $\identity{A}\in\surj{A}{A}$ by \cref{id_elem_surjections}. + $\identity{A}$ is injective by \cref{identity_injective}. + Follows by \cref{bijections}. +\end{proof} diff --git a/library/nat.tex b/library/nat.tex new file mode 100644 index 0000000..529ba54 --- /dev/null +++ b/library/nat.tex @@ -0,0 +1,21 @@ +\import{set/suc.tex} + + +\section{Natural numbers} + +\begin{abbreviation}\label{inductive_set} + $A$ is an inductive set iff $\emptyset\in A$ and for all $a\in A$ we have $\suc{a}\in A$. +\end{abbreviation} + +\begin{axiom}\label{naturals_inductive_set} + $\naturals$ is an inductive set. +\end{axiom} + +\begin{axiom}\label{naturals_smallest_inductive_set} + Let $A$ be an inductive set. + Then $\naturals\subseteq A$. +\end{axiom} + +\begin{abbreviation}\label{naturalnumber} + $n$ is a natural number iff $n\in\naturals$. +\end{abbreviation} diff --git a/library/order/order.tex b/library/order/order.tex new file mode 100644 index 0000000..339bad8 --- /dev/null +++ b/library/order/order.tex @@ -0,0 +1,102 @@ +\import{relation.tex} +\import{relation/properties.tex} +\import{order/quasiorder.tex} + +% also called "(partial) ordering" or "partial order" to contrast with connex (i.e. "total") orders. +\begin{abbreviation}\label{order} + $R$ is an order iff + $R$ is an antisymmetric quasiorder. +\end{abbreviation} + +\begin{abbreviation}\label{order_on} + $R$ is an order on $A$ iff + $R$ is an antisymmetric quasiorder on $A$. +\end{abbreviation} + +\begin{abbreviation}\label{strictorder} + $R$ is a strict order iff + $R$ is transitive and asymmetric. +\end{abbreviation} + +\begin{struct}\label{orderedset} + An ordered set $X$ is a quasiordered set + such that + \begin{enumerate} + \item\label{orderedset_antisym} $\lt[X]$ is antisymmetric. + \end{enumerate} +\end{struct} + +\begin{definition}\label{tostrictorder} + $\tostrictorder{R} = \{w\in R\mid \fst{w}\neq\snd{w}\}$. +\end{definition} + +\begin{definition}\label{toorder} + $\toorder{A}{R} = R\union\identity{A}$. +\end{definition} + +\begin{proposition}\label{tostrictorder_iff} + $(a,b)\in\tostrictorder{R}$ iff $(a,b)\in R$ and $a\neq b$. +\end{proposition} +\begin{proof} + Follows by \cref{tostrictorder,fst_eq,snd_eq}. +\end{proof} + +\begin{proposition}\label{toorder_reflexive} + $\toorder{A}{R}$ is reflexive on $A$. +\end{proposition} + +\begin{proposition}\label{toorder_intro} + Suppose $(a,b)\in R$. + Then $(a,b)\in\toorder{A}{R}$. +\end{proposition} +\begin{proof} + $R\subseteq\toorder{A}{R}$. +\end{proof} + +\begin{proposition}\label{toorder_elim} + Suppose $(a,b)\in\toorder{A}{R}$. + Then $(a,b)\in R$ or $a = b$. +\end{proposition} +\begin{proof} + Follows by \cref{toorder,id,union_iff,upair_intro_right,tostrictorder_iff}. +\end{proof} + +\begin{proposition}\label{toorder_iff} + $(a,b)\in\toorder{A}{R}$ iff $(a,b)\in R$ or $a = b\in A$. +\end{proposition} + +\begin{proposition}\label{strictorder_from_order} + Suppose $R$ is an order. + Then $\tostrictorder{R}$ is a strict order. +\end{proposition} +\begin{proof} + $\tostrictorder{R}$ is asymmetric. + $\tostrictorder{R}$ is transitive. +\end{proof} + +\begin{proposition}\label{order_from_strictorder} + Suppose $R$ is a strict order. + Suppose $R$ is a binary relation on $A$. + Then $\toorder{A}{R}$ is an order on $A$. +\end{proposition} +\begin{proof} + $\toorder{A}{R}$ is antisymmetric. + $\toorder{A}{R}$ is transitive by \cref{transitive,toorder_iff}. + $\toorder{A}{R}$ is reflexive on $A$. +\end{proof} + +\begin{proposition}\label{subseteqrel_antisymmetric} + $\subseteqrel{A}$ is antisymmetric. +\end{proposition} +\begin{proof} + Follows by \cref{subseteqrel,antisymmetric,pair_eq_iff,subseteq_antisymmetric}. +\end{proof} + + +\begin{proposition}\label{subseteqrel_is_order} + $\subseteqrel{A}$ is an order on $A$. +\end{proposition} +\begin{proof} + $\subseteqrel{A}$ is a quasiorder on $A$ by \cref{subseteqrel_is_quasiorder}. + $\subseteqrel{A}$ is antisymmetric by \cref{subseteqrel_antisymmetric}. +\end{proof} diff --git a/library/order/quasiorder.tex b/library/order/quasiorder.tex new file mode 100644 index 0000000..ab325e7 --- /dev/null +++ b/library/order/quasiorder.tex @@ -0,0 +1,51 @@ +\import{relation.tex} +\import{relation/properties.tex} + +\subsection{Quasiorders} + +% also called preorder +\begin{abbreviation}\label{quasiorder} + $R$ is a quasiorder iff + $R$ is quasireflexive and transitive. +\end{abbreviation} + +% also called preorder +\begin{abbreviation}\label{quasiorder_on} + $R$ is a quasiorder on $A$ iff + $R$ is a binary relation on $A$ and + $R$ is reflexive on $A$ and transitive. +\end{abbreviation} + +\begin{struct}\label{quasiordered_set} + A quasiordered set $X$ is a onesorted structure + equipped with + \begin{enumerate} + \item $\lt$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{quasiorder_type} $\lt[X]$ is a binary relation on $\carrier[X]$. + \item\label{quasiorder_refl} $\lt[X]$ is reflexive on $\carrier[X]$. + \item\label{quasiorder_tran} $\lt[X]$ is transitive. + \end{enumerate} +\end{struct} + +\begin{lemma}\label{quasiorder_transitive_double} + Let $X$ be a quasiordered set. + Let $a, b, c, d \in X$. + Suppose $a\mathrel{\lt[X]} b\mathrel{\lt[X]} c\mathrel{\lt[X]} d$. + Then $a\mathrel{\lt[X]} d$. +\end{lemma} +\begin{proof} + $\lt[X]$ is transitive. + Thus $a\mathrel{\lt[X]} c\mathrel{\lt[X]} d$ by \hyperref[transitive]{transitivity}. + Hence $a\mathrel{\lt[X]} d$ by \hyperref[transitive]{transitivity}. +\end{proof} + +\begin{proposition}\label{subseteqrel_is_quasiorder} + $\subseteqrel{A}$ is a quasiorder on $A$. +\end{proposition} +\begin{proof} + $\subseteqrel{A}$ is reflexive on $A$. + $\subseteqrel{A}$ is transitive. +\end{proof} diff --git a/library/order/semilattice.tex b/library/order/semilattice.tex new file mode 100644 index 0000000..51af68b --- /dev/null +++ b/library/order/semilattice.tex @@ -0,0 +1,41 @@ +\import{order/partial-order.tex} + +\begin{struct}\label{meet_semilattice} + A meet semilattice $X$ is a partial order + equipped with + \begin{enumerate} + \item $\meet$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{meet_type} for all $x,y\in \carrier[X]$ we have + $\meet[X](x,y)\in X$. + \item\label{meet_lb} for all $x,y\in \carrier[X]$ we have + $\meet[X](x,y) \mathrel{\lt[X]} x, y$. + \item\label{meet_glb} for all $a,x,y\in \carrier[X]$ such that $a\mathrel{\lt[X]} x, y$ we have + $a\mathrel{\lt[X]} \meet[X](x,y)$. + \end{enumerate} +\end{struct} + + +\begin{proposition}\label{meet_idempotent} + Let $X$ be a meet semilattice. + Then $\meet(x,x) = x$. +\end{proposition} +\begin{proof} + $\meet(x,x) \mathrel{\lt} x$. + $x\mathrel{\lt[X]} x, x$. + Thus $x\mathrel{\lt[X]} \meet(x,x)$. +\end{proof} + +%\begin{proposition}\label{meet_comm} +% Let $X$ be a meet semilattice. +% Suppose $x, y\in X$. +% Then $\meet(x,y) = \meet(y,x)$. +%\end{proposition} + +%\begin{proposition}\label{meet_assoc} +% Let $X$ be a meet semilattice. +% Suppose $x, y, z\in X$. +% Then $\meet(x,\meet(y,z)) = \meet(\meet(x,y),z)$. +%\end{proposition} diff --git a/library/ordinal.tex b/library/ordinal.tex new file mode 100644 index 0000000..3063162 --- /dev/null +++ b/library/ordinal.tex @@ -0,0 +1,638 @@ +\import{set.tex} +\import{set/cons.tex} +\import{set/powerset.tex} +\import{set/regularity.tex} +\import{set/suc.tex} +\import{nat.tex} + + +\section{Transitive sets} + +We use the word \emph{transitive} to talk about sets as relations, +so we will explicitly talk about \emph{\in-transitivity} here. + +% Here we have to ask TeX to forgive us for eliding the math +% mode around \in. We have to put the following into +% the preamble of our document: +% +% \let\mathonlyin\in +% \renewcommand{\in}{\ensuremath{\mathonlyin}} +% +\begin{definition}\label{transitiveset} + A set $A$ is \in-transitive iff for all $x, y$ + such that $x\in y\in A$ we have $x\in A$. +\end{definition} + +\begin{proposition}\label{transitiveset_iff_subseteq} + $A$ is \in-transitive iff + for all $a\in A$ we have $a\subseteq A$. +\end{proposition} + +\begin{proposition}\label{transitiveset_iff_pow} + $A$ is \in-transitive iff $A\subseteq \pow{A}$. +\end{proposition} +\begin{proof} + For all $a\in A$ we have $a\subseteq A \iff a\in\pow{A}$. + Follows by \cref{elem_subseteq,subseteq,pow_iff,transitiveset_iff_subseteq}. +\end{proof} + +\begin{proposition}\label{transitiveset_iff_unions_suc} + $A$ is \in-transitive iff $\unions{\suc{A}} = A$. +\end{proposition} +\begin{proof} + Follows by \cref{transitiveset,subseteq,subseteq_antisymmetric,suc,transitiveset_iff_pow,unions_subseteq_of_powerset_is_subseteq,unions_iff,suc_subseteq_intro,powerset_top}. +\end{proof} + +\begin{proposition}\label{transitiveset_iff_unions_subseteq} + $A$ is \in-transitive iff $\unions{A}\subseteq A$. +\end{proposition} + +\begin{proposition}\label{transitiveset_upair} + Suppose $A$ is \in-transitive. + Suppose $\{a,b\}\in A$. + Then $a,b\in A$. +\end{proposition} + +% For Kuratowski pairs only: +%\begin{proposition}\label{transitiveset_pair} +% Suppose $A$ is \in-transitive. +% Suppose $(a,b )\in A$. +% Then $a,b\in A$. +%\end{proposition} + +% For Kuratowski pairs only: +%\begin{proposition}\label{transitiveset_dom} +% Suppose $C$ is \in-transitive. +% Suppose $A\times B\subseteq C$. +% Suppose $b\in B$. +% Then $A\subseteq C$. +%\end{proposition} + +% For Kuratowski pairs only: +%\begin{proposition}\label{transitiveset_ran} +% Suppose $C$ is \in-transitive. +% Suppose $A\times B\subseteq C$. +% Suppose $a\in A$. +% Then $B\subseteq C$. +%\end{proposition} + +\subsubsection{Closure properties of \in-transitive sets} + +\begin{proposition}\label{emptyset_transitiveset} + $\emptyset$ is \in-transitive. +\end{proposition} + +\begin{proposition}\label{union_of_transitiveset_is_transitiveset} + Suppose $A$ and $B$ are \in-transitive. + Then $A\union B$ is \in-transitive. +\end{proposition} + +\begin{proposition}\label{inter_of_transitiveset_is_transitiveset} + Let $A, B$ be \in-transitive sets. + Then $A\inter B$ is \in-transitive. +\end{proposition} + +\begin{proposition}\label{suc_of_transitiveset_is_transitiveset} + Let $A$ be an \in-transitive set. + Then $\suc{A}$ is \in-transitive. +\end{proposition} + +\begin{proposition}\label{unions_of_transitiveset_is_transitiveset} + Let $A$ be an \in-transitive set. + Then $\unions{A}$ is \in-transitive. +\end{proposition} + +\begin{proposition}\label{unions_family_of_transitiveset_is_transitiveset} + Suppose every element of $A$ is an \in-transitive set. + Then $\unions{A}$ is \in-transitive. +\end{proposition} +\begin{proof} + Follows by \cref{transitiveset,unions_iff}. +\end{proof} + +\begin{proposition}\label{inters_family_of_transitiveset_is_transitiveset} + Suppose every element of $A$ is an \in-transitive set. + Then $\inters{A}$ is \in-transitive. +\end{proposition} +\begin{proof} + Follows by \cref{transitiveset,inters,unions_family_of_transitiveset_is_transitiveset}. +\end{proof} + + +\section{Ordinals} + +\begin{definition}\label{ordinal} + $\alpha$ is an ordinal iff + $\alpha$ is \in-transitive and + every element of $\alpha$ is \in-transitive. +\end{definition} + +\begin{proposition}\label{ordinal_intro} + Suppose $\alpha$ is \in-transitive. + Suppose every element of $\alpha$ is \in-transitive. + Then $\alpha$ is an ordinal. +\end{proposition} + +\begin{proposition}\label{ordinal_is_transitiveset} + Let $\alpha$ be an ordinal. + Then $\alpha$ is \in-transitive. +\end{proposition} + +\begin{proposition}\label{ordinal_elem_is_transitiveset} + Let $\alpha$ be an ordinal. + Suppose $A\in\alpha$. + Then $A$ is \in-transitive. +\end{proposition} + +\begin{proposition}\label{elem_of_ordinal_is_ordinal} + Let $\alpha$ be an ordinal. + Suppose $\beta\in\alpha$. + Then $\beta$ is an ordinal. +\end{proposition} + +\begin{proposition}\label{suc_ordinal_implies_ordinal} + Suppose $\suc{\alpha}$ is an ordinal. + Then $\alpha$ is an ordinal. +\end{proposition} + +\begin{proposition}\label{transitivesubseteq_of_ordinal_is_ordinal} + Let $\alpha$ be an ordinal. + Suppose $\beta\subseteq\alpha$. + Suppose $\beta$ is \in-transitive. + Then $\beta$ is an ordinal. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,ordinal}. +\end{proof} + +\begin{proposition}\label{ordinal_elem_implies_subseteq} + Let $\alpha,\beta$ be ordinals. + Suppose $\alpha\in\beta$. + Then $\alpha\subseteq\beta$. +\end{proposition} + +\begin{proposition}\label{ordinal_transitivity} + Let $\alpha$ be an ordinal. + Suppose $\gamma\in\beta\in\alpha$. + Then $\gamma\in\alpha$. +\end{proposition} +\begin{proof} + Follows by \cref{ordinal,transitiveset}. + % Vampire proof: Follows by \cref{ordinal,subseteq,transitiveset_iff_subseteq}. +\end{proof} + +\begin{proposition}\label{ordinal_suc_subseteq} + Let $\beta$ be an ordinal. + Suppose $\alpha\in\beta$. + Then $\suc{\alpha}\subseteq\beta$. +\end{proposition} + + +\begin{abbreviation}\label{ordinal_prec} + $\alpha \precedes \beta$ iff + $\beta$ is an ordinal and + $\alpha\in\beta$. +\end{abbreviation} + +\begin{abbreviation}\label{ordinal_preceq} + $\alpha\precedeseq \beta$ iff $\beta$ is an ordinal and $\alpha\subseteq\beta$. + % + %$\alpha\precedeseq \beta$ iff $\alpha\precedes\beta$ + %or $\alpha = \beta$ and $\beta$ is an ordinal. + % + %$\alpha\precedeseq \beta$ iff $\alpha\precedes\beta$ + %or $\beta$ is an ordinal equal to $\alpha$. +\end{abbreviation} + +\begin{lemma}\label{prec_is_ordinal} + Let $\alpha,\beta$ be sets. + Suppose $\alpha\precedes \beta$. + Then $\alpha$ is an ordinal. +\end{lemma} +\begin{proof} + Follows by \cref{elem_of_ordinal_is_ordinal}. +\end{proof} + +We already have global irreflexivity and asymmetry of \in. +\in\ is transitive on ordinals by definition. +To show that \in\ is a strict total order it only remains to show that \in\ is connex. + +\begin{proposition}\label{ordinal_elem_connex} + For all ordinals $\alpha,\beta$ + we have $\alpha\in\beta\lor \beta\in\alpha \lor \alpha = \beta$. +\end{proposition} +\begin{proof}[Proof by \in-induction on $\alpha$] + % Ind hypothesis: + % ![Xi,Xbeta]:(elem(Xi,falpha)=>((ordinal(Xi)&ordinal(Xbeta))=>(elem(Xi,Xbeta)|elem(Xbeta,Xi)|Xi=Xbeta)))) + % Goal: + % ordinal(falpha)&ordinal(fbeta))=>(elem(falpha,fbeta)|elem(fbeta,falpha)|falpha=fbeta) + % + Assume $\alpha$ is an ordinal. + Show for all ordinals $\gamma$ we have $\alpha\in\gamma\lor \gamma\in\alpha \lor \alpha = \gamma$. + \begin{subproof}[Proof by \in-induction on $\gamma$] + % Now we have: + % ![Xi]:(elem(Xi,fgamma)=>(ordinal(Xi)=>(elem(falpha,Xi)|elem(Xi,falpha)|falpha=Xi)))). + % Goal: ordinal(fgamma)=>(elem(falpha,fgamma)|elem(fgamma,falpha)|falpha=fgamma)) + % + Assume $\gamma$ is an ordinal. + % Goal: + % elem(falpha,fgamma)|elem(fgamma,falpha)|falpha=fgamma + % + % Original Vampire proof: + % Follows by \cref{setext,transitiveset,ordinal,in_implies_neq,prec_is_ordinal,in_asymmetric}. + % + % Pruned proof: + Follows by \cref{setext,transitiveset,ordinal}. + \end{subproof} +\end{proof} + +\begin{proposition}\label{ordinal_proper_subset_implies_elem} + Let $\alpha,\beta$ be ordinals. + Suppose $\alpha\subset\beta$. + Then $\alpha\in\beta$. +\end{proposition} +\begin{proof} + $\beta\setminus\alpha$ is inhabited. + Take $\gamma$ such that $\gamma$ is an \in-minimal element of $\beta\setminus\alpha$. + Now $\gamma\in\beta$ by \cref{setminus_elim_left}. + Hence $\gamma\subseteq\beta$ + by \cref{ordinal,transitiveset_iff_subseteq}. + For all $\delta\in\beta\setminus\alpha$ we have $\delta\notin\gamma$. + Thus $\gamma\setminus\alpha = \emptyset$. + Hence $\gamma\subseteq\alpha$. + It suffices to show that for all $\delta\in\alpha$ we have $\delta\in\gamma$. + Suppose not. + Take $\delta\in\alpha$ such that $\delta\notin\gamma$. + Now if $\delta = \gamma$ or $\gamma\in\delta$, then $\gamma\in\alpha$ + % Original Vampire proof: by \cref{ordinal,elem_subseteq,elem_of_ordinal_is_ordinal,setminus_elim_left,ordinal_elem_connex,inter_eq_left_implies_subseteq,inter_absorb_supseteq_left,transitiveset_iff_subseteq}. + by \cref{ordinal,elem_subseteq,elem_of_ordinal_is_ordinal,ordinal_elem_connex,transitiveset_iff_subseteq}. +\end{proof} + +\begin{proposition}\label{ordinal_elem_implies_proper_subset} + Let $\alpha,\beta$ be ordinals. + Suppose $\alpha\in\beta$. + Then $\alpha\subset\beta$. +\end{proposition} +\begin{proof} + $\alpha\subseteq\beta$. +\end{proof} + +\begin{proposition}\label{ordinal_preceq_implies_subseteq} +Let $\alpha,\beta$ be ordinals. +Suppose $\alpha\precedeseq\beta$. +Then $\alpha\subseteq\beta$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$\alpha = \beta$.} + Trivial. + \caseOf{$\alpha\precedes\beta$.} + $\alpha\subset\beta$. + \end{byCase} +\end{proof} + +%\begin{proposition}% +%\label{ordinal-subseteq-implies-preceq} +%Let $\alpha,\beta$ be ordinals. +%Suppose $\alpha\subseteq\beta$. +%Then $\alpha\precedeseq\beta$. +%\end{proposition} +%\begin{proof} +% \begin{byCase} +% \caseOf{$\alpha = \beta$.} +% Trivial. +% \caseOf{$\alpha\subset\beta$.} +% $\alpha\precedes\beta$. +% \end{byCase} +%\end{proof} + + +\begin{proposition}\label{ordinal_elem_or_subseteq} + Let $\alpha,\beta$ be ordinals. + Then $\alpha\in\beta$ or $\beta\subseteq\alpha$. +\end{proposition} + + +\begin{proposition}\label{ordinal_subseteq_or_subseteq} + Let $\alpha,\beta$ be ordinals. + Then $\alpha\subseteq\beta$ or $\beta\subseteq\alpha$. +\end{proposition} + + +\begin{proposition}\label{ordinal_subseteq_implies_elem_or_eq} + Let $\alpha,\beta$ be ordinals. + Suppose $\alpha\subseteq\beta$. + Then $\alpha\in\beta$ or $\alpha = \beta$. +\end{proposition} + + +\begin{corollary}\label{ordinal_subset_trichotomy} + Let $\alpha,\beta$ be ordinals. + Then $(\alpha\subset\beta \lor \beta\subset\alpha) \lor \alpha = \beta$. +\end{corollary} + +\begin{proposition}\label{ordinal_nor_elem_implies_eq} + Let $\alpha,\beta$ be ordinals. + Suppose neither $\alpha\in\beta$ nor $\beta\in\alpha$. + Then $\alpha = \beta$. +\end{proposition} +\begin{proof} + Neither $\alpha\subset\beta$ nor $\beta\subset\alpha$. +\end{proof} + +\begin{proposition}\label{ordinal_in_trichotomy} + Let $\alpha,\beta$ be ordinals. Then $(\alpha\in\beta \lor \beta\in\alpha) \lor \alpha = \beta$. +\end{proposition} +\begin{proof} + Suppose not. + Then neither $\alpha\in\beta$ nor $\beta\in\alpha$. + Thus $\alpha = \beta$ by \cref{ordinal_nor_elem_implies_eq}. Contradiction. +\end{proof} + +\begin{corollary}\label{ordinal_prec_trichotomy} + Let $\alpha,\beta$ be ordinals. + Suppose neither $\alpha\precedes\beta$ nor $\beta\precedes\alpha$. + Then $\alpha = \beta$. +\end{corollary} +\begin{proof} + Follows by \cref{ordinal_nor_elem_implies_eq}. +\end{proof} + +\begin{corollary}\label{ordinal_elem_or_superset} + Let $\alpha,\beta$ be ordinals. Then $\alpha\in \beta$ or $\beta\subseteq \alpha$. +\end{corollary} + + + +\subsubsection{Construction of ordinals} + +\begin{proposition}\label{emptyset_is_ordinal} + $\emptyset$ is an ordinal. +\end{proposition} + +% The proof of this theorem benefits from the alternate definition of +% transitivity in terms of $\subseteq$. +\begin{proposition}\label{suc_ordinal} + Let $\alpha$ be an ordinal. + $\suc{\alpha}$ is an ordinal. +\end{proposition} +\begin{proof} + $\suc{\alpha}$ is \in-transitive by \cref{ordinal,suc_of_transitiveset_is_transitiveset}. + For every $\beta\in\alpha$ we have that $\beta$ is \in-transitive. +\end{proof} + +\begin{proposition}\label{ordinal_iff_suc_ordinal} + $\alpha$ is an ordinal iff $\suc{\alpha}$ is an ordinal. +\end{proposition} + +\begin{proposition}\label{ordinal_in_suc} + Let $\alpha$ be an ordinal. + Then $\alpha\in\suc{\alpha}$. +\end{proposition} + +\begin{corollary}\label{ordinal_precedes_suc} + Let $\alpha$ be an ordinal. + Then $\alpha\precedes \suc{\alpha}$. +\end{corollary} + +\begin{proposition}\label{ordinal_elem_implies_subset_of_suc} + Let $\alpha,\beta$ be ordinals. + Suppose $\alpha\in\beta$. + Then $\alpha\subseteq\suc{\beta}$. +\end{proposition} +\begin{proof} + $\alpha\subset \beta$. + In particular, $\alpha\subseteq \beta$. + Hence $\alpha\subseteq \cons{\beta}{\beta}$. +\end{proof} + +\begin{proposition}\label{unions_of_ordinal_is_ordinal} + Let $\alpha$ be an ordinal. + Then $\unions{\alpha}$ is an ordinal. +\end{proposition} +\begin{proof} + For all $x, y$ such that $x\in y\in \unions{\alpha}$ we have $x\in \unions{\alpha}$ + by \cref{unions_intro,unions_iff,transitiveset,ordinal}. + Thus $\unions{\alpha}$ is \in-transitive. + Every element of $\unions{\alpha}$ is \in-transitive. +\end{proof} + +\begin{lemma}\label{ordinal_subseteq_unions} + Let $\alpha$ be an ordinal. + Then $\unions{\alpha}\subseteq \alpha$. +\end{lemma} +\begin{proof} + Follows by \cref{ordinal,transitiveset_iff_unions_subseteq}. +\end{proof} + +\begin{proposition}\label{union_of_two_ordinals_is_ordinal} + Let $\alpha,\beta$ be ordinals. + Then $\alpha\union\beta$ is an ordinal. +\end{proposition} +\begin{proof} + $\alpha\union\beta$ is \in-transitive by \cref{union_of_transitiveset_is_transitiveset,ordinal}. + Every element of $\alpha\union\beta$ is \in-transitive + by \cref{transitiveset,union_iff,ordinal}. + Follows by \cref{ordinal}. +\end{proof} + +\begin{proposition}\label{ordinal_empty_or_emptyset_elem} + For all ordinals $\alpha$ + we have $\alpha=\emptyset$ or $\emptyset\in\alpha$. +\end{proposition} +\begin{proof}[Proof by \in-induction] + Straightforward. +\end{proof} + +\begin{proposition}\label{transitive_set_of_ordinals_is_ordinal} + Let $A$ be a set. + Suppose that for every $\alpha\in A$ we have $\alpha$ is an ordinal. + Suppose that $A$ is \in-transitive. + Then $A$ is an ordinal. +\end{proposition} + +% Apparently Russel first noticed this antimony while reading a paper by Burali-Forti. +% Typographic NB: Cesare Burali-Forti is a single person, therefore only a single hyphen! +\begin{theorem}[Burali-Forti antimony]\label{buraliforti_antinomy} + There exists no set $\Omega$ such that + for all $\alpha$ we have $\alpha\in \Omega$ iff $\alpha$ is an ordinal. +\end{theorem} +\begin{proof} + Suppose not. + Take $\Omega$ such that for all $\alpha$ we have $\alpha\in \Omega$ iff $\alpha$ is an ordinal. + For all $x, y$ such that $x\in y\in \Omega$ we have $x\in \Omega$. + Thus $\Omega$ is \in-transitive. + Thus $\Omega$ is an ordinal. + Therefore $\Omega\in\Omega$. + Contradiction. +\end{proof} + +\begin{proposition}\label{inters_of_ordinals_is_ordinal} + Let $A$ be an inhabited set. + Suppose for every $\alpha\in A$ we have $\alpha$ is an ordinal. + Then $\inters{A}$ is an ordinal. +\end{proposition} +\begin{proof} + It suffices to show that $\inters{A}$ is \in-transitive. +\end{proof} + +\begin{proposition}\label{inters_of_ordinals_subseteq} + Let $A$ be an inhabited set. + Suppose for every $\alpha\in A$ we have $\alpha$ is an ordinal. + Then for all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$. +\end{proposition} + +\begin{proposition}\label{inters_of_ordinals_elem} + Let $A$ be an inhabited set. + Suppose for every $\alpha\in A$ we have $\alpha$ is an ordinal. + Then $\inters{A}\in A$. +\end{proposition} +\begin{proof} + % Vampire proof: + Follows by \cref{inters_of_ordinals_is_ordinal,in_implies_neq,inters_iff_forall,ordinal_subseteq_implies_elem_or_eq,inters_subseteq_elem}. +\end{proof} + +\begin{proposition}\label{inters_of_ordinals_is_minimal} + Let $A$ be an inhabited set. + Suppose for every $\alpha\in A$ we have $\alpha$ is an ordinal. + Then $\inters{A}$ is an \in-minimal element of $A$. +\end{proposition} +\begin{proof} + For all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$. +\end{proof} + +\begin{proposition}\label{inters_of_ordinals_is_minimal_alternate} + Let $A$ be an inhabited set. + Suppose for every $\alpha\in A$ we have $\alpha$ is an ordinal. + Then for all $\alpha\in A$ we have $\inters{A} = \alpha$ or $\inters{A}\in\alpha$. +\end{proposition} +\begin{proof} + For all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$. +\end{proof} + +\begin{proposition}\label{inter_of_two_ordinals_is_ordinal} + Let $\alpha,\beta$ be ordinals. + Then $\alpha\inter\beta$ is an ordinal. + \end{proposition} +\begin{proof} + $\alpha\inter\beta$ is \in-transitive by \cref{inter,ordinal,transitiveset}. + Every element of $\alpha\inter\beta$ is \in-transitive + by \cref{transitiveset,inter,ordinal}. + Follows by \cref{ordinal}. +\end{proof} + + +\subsubsection{Limit and successor ordinals} + + +\begin{definition}\label{limit_ordinal} + $\lambda$ is a limit ordinal iff + $\emptyset\precedes \lambda$ % by definition of \precedes this means that $\lambda$ is an ordinal + and for all $\alpha\in \lambda$ we have $\suc{\alpha}\in \lambda$. +\end{definition} + +\begin{definition}\label{successor_ordinal} + $\alpha$ is a successor ordinal iff + there exists an ordinal $\beta$ such that $\alpha = \suc{\beta}$. +\end{definition} + +\begin{lemma}\label{positive_ordinal_is_limit_or_successor} + Let $\alpha$ be an ordinal such that $\emptyset\precedes\alpha$. + Then $\alpha$ is a limit ordinal or $\alpha$ is a successor ordinal. +\end{lemma} +\begin{proof} + \begin{byCase} + \caseOf{$\alpha$ is a limit ordinal.} + Trivial. + \caseOf{$\alpha$ is not a limit ordinal.} + Take $\beta$ such that $\beta\in\alpha$ and $\suc{\beta}\notin\alpha$ + by \cref{limit_ordinal}. + \end{byCase} +\end{proof} + +\begin{lemma}\label{zero_not_successorordinal} + $\emptyset$ is not a successor ordinal. +\end{lemma} + +\begin{lemma}\label{zero_not_limitordinal} + $\emptyset$ is not a limit ordinal. +\end{lemma} +\begin{proof} + Suppose not. + Then $\emptyset\precedes \emptyset$ by \cref{notin_emptyset,limit_ordinal}. + Thus $\emptyset\in \emptyset$. + Contradiction. +\end{proof} + +\begin{lemma}\label{suc_elem_limitordinal} + Let $\lambda$ be a limit ordinal. + Let $\alpha\in\lambda$. + Then $\suc{\alpha}\in\lambda$. +\end{lemma} +\begin{proof} + Follows by \cref{limit_ordinal}. +\end{proof} + +\begin{lemma}\label{limitordinal_eq_unions} + Let $\lambda$ be a limit ordinal. + Then $\unions{\lambda} = \lambda$. +\end{lemma} +\begin{proof} + $\unions{\lambda}\subseteq\lambda$ by \cref{limit_ordinal,ordinal_subseteq_unions}. + For all $\alpha\in\lambda$ we have $\alpha\in\suc{\alpha}\in\lambda$ by \cref{suc_intro_self,suc_elem_limitordinal}. + Thus $\lambda\subseteq\unions{\lambda}$ by \cref{subseteq,unions_intro}. + Follows by \cref{subseteq_antisymmetric}. +\end{proof} + + +\subsection{Natural numbers as ordinals} + +\begin{lemma}\label{nat_is_successor_ordinal} + Let $n\in\naturals$. + Suppose $n\neq \emptyset$. + Then $n$ is a successor ordinal. +\end{lemma} +\begin{proof} + Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$. + $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}. + Now $M\subseteq \naturals\subseteq M$ + by \cref{subseteq,naturals_smallest_inductive_set}. + Thus $M = \naturals$. + Follows by \cref{subseteq}. +\end{proof} + +\begin{lemma}\label{nat_is_transitiveset} + $\naturals$ is \in-transitive. +\end{lemma} +\begin{proof} + Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$. + $\emptyset\in M$. + For all $n\in M$ we have $\suc{n}\in M$ + by \cref{naturals_inductive_set,suc}. + Thus $M$ is an inductive set. + Now $M\subseteq \naturals\subseteq M$ + by \cref{subseteq,naturals_smallest_inductive_set}. + Hence $\naturals = M$. +\end{proof} + +\begin{lemma}\label{natural_number_is_ordinal} + Every natural number is an ordinal. +\end{lemma} +\begin{proof} + Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}. +\end{proof} + +\begin{lemma}\label{omega_is_an_ordinal} + $\naturals$ is an ordinal. +\end{lemma} +\begin{proof} + Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}. +\end{proof} + +\begin{lemma}\label{omega_is_a_limit_ordinal} + $\naturals$ is a limit ordinal. +\end{lemma} +\begin{proof} + $\emptyset\precedes \naturals$. + If $n\in \naturals$, then $\suc{n}\in\naturals$. +\end{proof} diff --git a/library/relation.tex b/library/relation.tex new file mode 100644 index 0000000..b5aebcd --- /dev/null +++ b/library/relation.tex @@ -0,0 +1,1081 @@ +\import{set.tex} +\import{set/powerset.tex} +\import{set/product.tex} + +\section{Relations} + +\begin{definition}\label{relation} + $R$ is a relation iff + for all $w\in R$ there exists $x, y$ such that $w = (x, y)$. +\end{definition} + +\begin{definition}\label{comparable} + $a$ is comparable with $b$ in $R$ iff $a\mathrel{R}b$ or $b\mathrel{R}a$. +\end{definition} + +\begin{proposition}\label{relext} + Let $R, S$ be relations. + Suppose for all $x,y$ we have $x\mathrel{R} y$ iff $x\mathrel{S} y$. + Then $R = S$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{abbreviation}\label{family_of_relations} + $F$ is a family of relations iff + every element of $F$ is a relation. +\end{abbreviation} + +\begin{proposition}\label{unions_of_family_of_relations_is_relation} + Let $F$ be a family of relations. + Then $\unions{F}$ is a relation. +\end{proposition} + +\begin{proposition}\label{inters_of_family_of_relations_is_relation} + Let $F$ be a family of relations. + Then $\inters{F}$ is a relation. +\end{proposition} + +\begin{proposition}\label{union_relations_is_relation} + Let $R, S$ be relations. + Then $R\union S$ is a relation. +\end{proposition} + +\begin{proposition}\label{union_relations_is_relation_type} + Suppose $R\subseteq A\times B$. + Suppose $S\subseteq C\times D$. + Then $R\union S\subseteq (A\union C)\times (B\union D)$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,union_times_elim,union_iff,union_subseteq_union}. +\end{proof} + +\begin{proposition}\label{inter_relations_is_relation} + Let $R, S$ be relations. + Then $R\inter S$ is a relation. +\end{proposition} + +\begin{proposition}\label{setminus_relations_is_relation} + Let $R, S$ be relations. + Then $R\setminus S$ is a relation. +\end{proposition} + + + +\subsection{Converse of a relation} + +\begin{definition}\label{converse_relation} + $\converse{R} = \{ z\mid \exists w\in R. \exists x, y. w = (x, y)\land z = (y, x)\}$. +\end{definition} + +\begin{proposition}\label{converse_intro} + If $y\mathrel{R} x$, then $x\mathrel{\converse{R}} y$. +\end{proposition} + +\begin{proposition}\label{converse_elim} + If $x\mathrel{\converse{R}} y$, then $y\mathrel{R} x$. +\end{proposition} + +\begin{proposition}\label{converse_iff} + $x\mathrel{\converse{R}} y$ iff $y\mathrel{R} x$. +\end{proposition} + + +\begin{proposition}\label{converse_is_relation} + $\converse{R}$ is a relation. +\end{proposition} + + +\begin{proposition}\label{converse_converse_iff} + $x \mathrel{\converse{\converse{R}}} y$ iff $x\mathrel{R} y$. +\end{proposition} + +% Only works if the starting set was a relation (i.e. only has pairs as elements). +\begin{proposition}\label{converse_converse_eq} + Let $R$ be a relation. + Then $\converse{\converse{R}} = R$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{converse_type} + Suppose $R\subseteq A\times B$. + Then $\converse{R}\subseteq B\times A$. +\end{proposition} +\begin{proof} + It suffices to show that every element of $\converse{R}$ is an element of $B\times A$ + by \cref{subseteq}. + Fix $w\in\converse{R}$. + Take $x, y$ such that $w = (y, x)$ and $x\mathrel{R} y$ by \cref{converse_relation}. + Now $(x,y)\in A\times B$ by \cref{subseteq}. + Thus $x\in A$ and $y\in B$ by \cref{times_tuple_elim}. + Hence $(y,x)\in B\times A$ by \cref{times_tuple_intro}. +\end{proof} + +\begin{proposition}\label{converse_times} + Then $\converse{B\times A} = A\times B$. +\end{proposition} +\begin{proof} + For all $w$ we have $w\in\converse{B\times A}$ iff $w\in A\times B$ + by \cref{converse_relation,times,times_elem_is_tuple,times_tuple_elim}. + Follows by \hyperref[setext]{extensionality}. + %Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{converse_emptyset} + Then $\converse{\emptyset} = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{converse_subseteq_intro} + Let $R$ be a relation. + If $R\subseteq S$, then $\converse{R}\subseteq\converse{S}$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,converse_relation,relation}. +\end{proof} + +\begin{proposition}\label{converse_subseteq_elim} + Let $R$ be a relation. + If $\converse{R}\subseteq\converse{S}$, then $R\subseteq S$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,converse_relation,relation,converse_subseteq_intro,converse_converse_iff}. +\end{proof} + +\begin{proposition}\label{converse_subseteq_iff} + Let $R$ be a relation. + $\converse{R}\subseteq\converse{S}$ iff $R\subseteq S$. +\end{proposition} +\begin{proof} + Follows by \cref{converse_subseteq_elim,converse_subseteq_intro}. +\end{proof} + +\begin{proposition}\label{converse_union} + $\converse{(R\union S)} = \converse{R}\union\converse{S}$. +\end{proposition} +\begin{proof} + $\converse{(R\union S)}$ is a relation by \cref{converse_is_relation}. + $\converse{R}\union\converse{S}$ is a relation by \cref{converse_is_relation,union_relations_is_relation}. + For all $a,b$ we have $(a,b)\in\converse{(R\union S)}$ iff $(a,b)\in\converse{R}\union\converse{S}$ + by \cref{union_iff,converse_iff}. + Follows by \hyperref[relext]{extensionality}. +\end{proof} + +\begin{proposition}\label{converse_inter} + $\converse{(R\inter S)} = \converse{R}\inter\converse{S}$. +\end{proposition} +\begin{proof} + $\converse{(R\inter S)}$ is a relation by \cref{converse_is_relation}. + $\converse{R}\inter\converse{S}$ is a relation by \cref{converse_is_relation,inter_relations_is_relation}. + For all $a,b$ we have $(a,b)\in\converse{(R\inter S)}$ iff $(a,b)\in\converse{R}\inter\converse{S}$ + by \cref{inter,converse_iff}. + Follows by \hyperref[relext]{extensionality}. +\end{proof} + +\begin{proposition}\label{converse_setminus} + $\converse{(R\setminus S)} = \converse{R}\setminus\converse{S}$. +\end{proposition} +\begin{proof} + $\converse{(R\setminus S)}$ is a relation by \cref{converse_is_relation}. + $\converse{R}\setminus\converse{S}$ is a relation by \cref{converse_is_relation,setminus_relations_is_relation}. + For all $a,b$ we have $(a,b)\in\converse{(R\setminus S)}$ iff $(a,b)\in\converse{R}\setminus\converse{S}$. + Follows by \hyperref[relext]{extensionality}. +\end{proof} + + + +\subsubsection{Domain of a relation} + +\begin{definition}\label{dom} + $\dom{R} = \{ x\mid \exists w\in R. \exists y. w = (x, y)\}$. +\end{definition} + +\begin{proposition}\label{dom_iff} + $a\in\dom{R}$ iff there exists $b$ such that $a\mathrel{R} b$. +\end{proposition} + +\begin{proposition}\label{dom_intro} + Suppose $a\mathrel{R} b$. + Then $a\in\dom{R}$. +\end{proposition} +\begin{proof} + Follows by \cref{dom_iff}. +\end{proof} + +\begin{proposition}\label{dom_emptyset} + $\dom{\emptyset} = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{dom_times} + $\dom{(A\times B)}\subseteq A$. +\end{proposition} + +\begin{proposition}\label{dom_times_inhabited} + Suppose $b\in B$. + $\dom{(A\times B)} = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{dom_cons} + $\dom{\cons{(a,b)}{R}} = \cons{a}{\dom{R}}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{dom_union} + $\dom{(A\union B)} = \dom{A}\union\dom{B}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{dom_inter} + $\dom{(A\inter B)}\subseteq \dom{A}\inter\dom{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,inter,dom_iff}. +\end{proof} + +\begin{proposition}\label{dom_setminus} + $\dom{(A\setminus B)}\supseteq \dom{A}\setminus\dom{B}$. +\end{proposition} + +% TODO (also needs to import set/cons) +%\begin{proposition}\label{dom_remove_invariant} +% Suppose $a\mathrel{R}b$. +% Suppose $b\neq c$. +% Then $\dom{\remove{(a,b)}{R}} = \dom{R}$. +%\end{proposition} + +\subsubsection{Range of a relation} + +\begin{definition}\label{ran} + $\ran{R} = \{ y\mid \exists w\in R. \exists x. w = (x, y)\}$. +\end{definition} + +\begin{proposition}\label{ran_iff} + $b\in\ran{R}$ iff there exists $a$ such that $a\mathrel{R} b$. +\end{proposition} + +\begin{proposition}\label{ran_intro} + Suppose $a\mathrel{R} b$. + Then $b\in\ran{R}$. +\end{proposition} +\begin{proof} + Follows by \cref{ran_iff}. +\end{proof} + +\begin{proposition}\label{ran_emptyset} + $\ran{\emptyset} = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{ran_times} + $\ran{(A\times B)}\subseteq B$. +\end{proposition} + +\begin{proposition}\label{ran_times_inhabited} + Suppose $a\in A$. + $\ran{(A\times B)} = B$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{ran_cons} + $\ran{(\cons{(a,b)}{R})} = \cons{b}{\ran{R}}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{ran_union} + $\ran{(A\union B)} = \ran{A}\union\ran{B}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{ran_inter} + $\ran{(A\inter B)}\subseteq \ran{A}\inter\ran{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,inter,ran_iff}. +\end{proof} + +\begin{proposition}\label{ran_setminus} + $\ran{(A\setminus B)}\supseteq \ran{A}\setminus\ran{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,setminus,ran_iff}. +\end{proof} + +\subsubsection{Domain and range of converse} + +\begin{proposition}\label{dom_converse} + $\dom{\converse{R}} = \ran{R}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{ran_converse} + $\ran{\converse{R}} = \dom{R}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + + +\subsubsection{Field of a relation} + +% We ues fld for the label instead of field so that field stays available for the +% algebraic structure. +\begin{definition}\label{fld} + $\fld{R} = \dom{R}\union\ran{R}$. +\end{definition} + +\begin{proposition}\label{fld_iff} + $c\in\fld{R}$ iff there exists $d$ such that $c\mathrel{R}d$ or $d\mathrel{R}c$. +\end{proposition} +\begin{proof} + Follows by \cref{fld,dom_iff,ran_iff,union_iff}. +\end{proof} + +\begin{proposition}\label{fld_intro_left} + Suppose $(a,b)\in R$. + Then $a\in\fld{R}$. +\end{proposition} +\begin{proof} + Follows by \cref{fld,dom,union_iff}. +\end{proof} + +\begin{proposition}\label{fld_intro_right} + Suppose $(a,b)\in R$. + Then $b\in\fld{R}$. +\end{proposition} +\begin{proof} + Follows by \cref{fld,ran,union_iff}. +\end{proof} + +\begin{proposition}\label{dom_subseteq_fld} + Then $\dom{R}\subseteq\fld{R}$. +\end{proposition} +\begin{proof} + Follows by \cref{fld,union_upper_left}. +\end{proof} + +\begin{proposition}\label{ran_subseteq_fld} + Then $\ran{R}\subseteq\fld{R}$. +\end{proposition} +\begin{proof} + Follows by \cref{fld,union_upper_right}. +\end{proof} + +\begin{proposition}\label{fld_times} + $\fld{(A\times B)}\subseteq A\union B$. +\end{proposition} +\begin{proof} + Follows by \cref{fld,dom_times,ran_times,union_subseteq_union}. +\end{proof} + +\begin{proposition}\label{relation_elem_times_fld} + Let $R$ be a relation. + Suppose $w\in R$. + Then $w\in\fld{R}\times\fld{R}$. +\end{proposition} +\begin{proof} + Take $a,b$ such that $w = (a, b)$ by \cref{relation}. + Then $a,b\in\fld{R}$ by \cref{fld_iff}. + Thus $(a,b)\in\fld{R}\times\fld{R}$ by \cref{times_tuple_intro}. +\end{proof} + +\begin{proposition}\label{relation_subseteq_times_fld} + Let $R$ be a relation. + Then $R\subseteq\fld{R}\times\fld{R}$. +\end{proposition} +\begin{proof} + Follows by \cref{relation_elem_times_fld,subseteq}. +\end{proof} + +\begin{proposition}\label{fld_universal} + $\fld{(A\times A)} = A$. +\end{proposition} + +\begin{proposition}\label{fld_emptyset} + $\fld{\emptyset} = \emptyset$. +\end{proposition} + +\begin{proposition}\label{fld_cons} + $\fld{(\cons{(a,b)}{R})} = \cons{a}{\cons{b}{\fld{R}}}$. +\end{proposition} + +\begin{proposition}\label{fld_union} + $\fld{(A\union B)} = \fld{A}\union\fld{B}$. +\end{proposition} +\begin{proof} + \begin{align*} + \fld{(A\union B)} + &= \dom{(A\union B)}\union\ran{(A\union B)} + \explanation{by \cref{fld}}\\ + &= (\dom{A}\union\dom{B})\union(\ran{A}\union\ran{B}) + \explanation{by \cref{dom_union,ran_union}}\\ + &= (\dom{A}\union\ran{A})\union(\dom{B}\union\ran{B}) + \explanation{by \cref{union_comm,union_assoc}}\\ + &= \fld{A}\union\fld{B} + \explanation{by \cref{fld}} + \end{align*} +\end{proof} + +\begin{proposition}\label{fld_inter} + $\fld{(A\inter B)}\subseteq \fld{A}\inter\fld{B}$. +\end{proposition} +\begin{proof} + % LATER this is surprisingly slow because the ATP can generate lots of nested intersection terms. + Follows by \cref{subseteq,fld_iff,subseteq_inter_iff}. +\end{proof} + +\begin{proposition}\label{fld_setminus} + $\fld{(A\setminus B)}\supseteq \fld{A}\setminus\fld{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{setminus_subseteq,fld_iff,subseteq,setminus}. +\end{proof} + +\begin{proposition}\label{fld_converse} + $\fld{\converse{R}} = \fld{R}$. +\end{proposition} +\begin{proof} + Follows by \cref{fld,dom_converse,ran_converse,union_comm}. +\end{proof} + + +\subsection{Image} + +\begin{definition}\label{img} + $\img{R}{A} = \{b\in\ran{R} \mid \exists a\in A. a\mathrel{R} b \}$. +\end{definition} + +\begin{proposition}\label{img_elem_intro} + Suppose $a\in A$ and $a\mathrel{R} b$. + Then $b\in\img{R}{A}$. +\end{proposition} +\begin{proof} + Follows by \cref{img,ran}. +\end{proof} + +\begin{proposition}\label{img_iff} + $b\in\img{R}{A}$ iff there exists $a\in A$ such that $a\mathrel{R} b$. +\end{proposition} + +\begin{proposition}\label{img_subseteq} + Suppose $A\subseteq B$. + Then $\img{R}{A}\subseteq \img{R}{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,img_iff}. +\end{proof} + +\begin{proposition}\label{img_subseteq_ran} + Then $\img{R}{A}\subseteq \ran{R}$. +\end{proposition} + +\begin{proposition}\label{img_dom} + Then $\img{R}{\dom{R}} = \ran{R}$. +\end{proposition} + +\begin{proposition}\label{img_union} + $\img{R}{A\union B} = \img{R}{A}\union\img{R}{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{setext,union_iff,img_iff}. +\end{proof} + +\begin{proposition}\label{img_inter} + % Equality does not hold in general + $\img{R}{A\inter B}\subseteq \img{R}{A}\inter\img{R}{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{img_iff,subseteq,inter}. +\end{proof} + +\begin{proposition}\label{img_setminus} + % Equality does not hold in general + $\img{R}{A\setminus B}\supseteq \img{R}{A}\setminus\img{R}{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{img_iff,subseteq,setminus}. +\end{proof} + +\begin{proposition}\label{img_singleton_iff} + $b\in \img{R}{\{a\}}$ iff $a\mathrel{R}b$. +\end{proposition} + +\begin{proposition}\label{img_singleton_intro} + Suppose $b\in\img{R}{\{a\}}$. + Then $b\in\ran{R}$ and $(a,b)\in R$. +\end{proposition} +\begin{proof} + Follows by \cref{img_iff,singleton_iff,img_subseteq_ran,elem_subseteq}. +\end{proof} + +\begin{proposition}\label{img_singleton} + $\img{R}{\{a\}} = \{b\in\ran{R}\mid (a,b)\in R \}$. +\end{proposition} + +\begin{proposition}\label{img_emptyset} + $\img{R}{\emptyset} = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\subsection{Preimage} + +\begin{definition}\label{preimg} + $\preimg{R}{B} = \{a\in\dom{R} \mid \exists b\in B. a\mathrel{R} b \}$. +\end{definition} + +\begin{proposition}\label{preimg_iff} + $a\in\preimg{R}{B}$ iff there exists $b\in B$ such that $a\mathrel{R} b$. +\end{proposition} + +\begin{proposition}\label{preim_eq_img_of_converse} + $\preimg{R}{B} = \img{\converse{R}}{B}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{preimg_subseteq} + Suppose $A\subseteq B$. + Then $\preimg{R}{A}\subseteq \preimg{R}{B}$. +\end{proposition} + +\begin{proposition}\label{preimg_subseteq_dom} + Then $\preimg{R}{A}\subseteq \dom{R}$. +\end{proposition} + +\begin{proposition}\label{preimg_union} + $\preimg{R}{A\union B} = \preimg{R}{A}\union\preimg{R}{B}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{preimg_inter} + % Equality does not hold in general + $\preimg{R}{A\inter B}\subseteq \preimg{R}{A}\inter\preimg{R}{B}$. +\end{proposition} + +\begin{proposition}\label{preimg_setminus} + % Equality does not hold in general + $\preimg{R}{A\setminus B}\supseteq \preimg{R}{A}\setminus\preimg{R}{B}$. +\end{proposition} + +\subsection{Upward and downward closure} + +\begin{definition}\label{upward_closure} + $\upward{R}{a} = \{b\in\ran{R} \mid a\mathrel{R}b \}$. +\end{definition} + +\begin{definition}\label{downward_closure} + $\downward{R}{b} = \{a\in\dom{R} \mid a\mathrel{R}b \}$. +\end{definition} + +\begin{proposition}\label{downward_closure_iff} + $a\in\downward{R}{b}$ iff $a\mathrel{R}b$. +\end{proposition} + +\subsection{Relation (and later also function) composition} + +Composition ignores the non-relational parts of sets. +Note that the order is flipped from usual relation composition. +This lets us use the same symbol for composition of functions. + +\begin{definition}\label{circ} + $S\circ R = \{ (x,z)\mid x\in\dom{R}, z\in\ran{S}\mid \exists y.\ x\mathrel{R}y\mathrel{S}z \}$. +\end{definition} + +\begin{proposition}\label{circ_is_relation} + $S\circ R$ is a relation. +\end{proposition} + +\begin{proposition}\label{circ_elem_intro} + Suppose $x\mathrel{R} y\mathrel{S} z$. + Then $x\mathrel{(S\circ R)} z$. +\end{proposition} +\begin{proof} + $x\in\dom{R}$ and $z\in\ran{S}$. + Then $(x, z)\in S\circ R$ by \cref{circ}. +\end{proof} + +\begin{proposition}\label{circ_elem_elim} + Suppose $x\mathrel{(S\circ R)} z$. + Then there exists $y$ such that $x\mathrel{R} y\mathrel{S} z$. +\end{proposition} +\begin{proof} + %$x\in\dom{R}$ and $z\in\ran{S}$. + There exists $y$ such that $x\mathrel{R} y\mathrel{S} z$ by \cref{circ,pair_eq_iff}. +\end{proof} + +\begin{proposition}\label{circ_iff} + $x\mathrel{(S\circ R)} z$ iff there exists $y$ such that $x\mathrel{R} y\mathrel{S} z$. +\end{proposition} + +\begin{proposition}\label{circ_assoc} + $(T\circ S)\circ R = T\circ (S\circ R)$. +\end{proposition} +\begin{proof} + For all $a, b$ we have + $(a,b)\in (T\circ S)\circ R$ iff $(a,b)\in T\circ (S\circ R)$ + by \cref{circ_iff}. + Now $(T\circ S)\circ R$ is a relation and $T\circ (S\circ R)$ is a relation by + \cref{circ_is_relation}. + Follows by \hyperref[relext]{relation extensionality}. +\end{proof} + +\begin{proposition}\label{circ_converse_intro_tuple} + Suppose $(a, c) \in\converse{R}\circ\converse{S}$. + Then $(a,c)\in \converse{(S\circ R)}$. +\end{proposition} +\begin{proof} + Take $b$ such that $a\mathrel{\converse{S}} b\mathrel{\converse{R}} c$. + Now $c\mathrel{R}b\mathrel{S} a$ by \cref{converse_iff}. + Hence $c\mathrel{(S\circ R)} a$. + Thus $a\mathrel{\converse{(S\circ R)}} c$. +\end{proof} + +\begin{proposition}\label{circ_converse_elim} + Suppose $(a,c)\in \converse{(S\circ R)}$. + Then $(a, c) \in\converse{R}\circ\converse{S}$. +\end{proposition} +\begin{proof} + $c\mathrel{(S\circ R)} a$. + Take $b$ such that $c\mathrel{R}b\mathrel{S} a$. + Now $a\mathrel{\converse{S}} b\mathrel{\converse{R}} c$. +\end{proof} + +\begin{proposition}\label{circ_converse} + $\converse{(S\circ R)} = \converse{R}\circ\converse{S}$. +\end{proposition} +\begin{proof} + $\converse{(S\circ R)}$ is a relation. + $\converse{R}\circ\converse{S}$ is a relation. + For all $x, y $ we have $(x,y)\in \converse{(S\circ R)}$ iff $(x, y) \in\converse{R}\circ\converse{S}$. + Thus $\converse{(S\circ R)} = \converse{R}\circ\converse{S}$ by \cref{relext}. +\end{proof} + +\subsection{Restriction} + +\begin{definition}% +\label{restrl} + $\restrl{R}{X} = \{ w\in R \mid \exists x, y. x\in X \land w = (x, y) \}$. +\end{definition} + +\begin{proposition}\label{restrl_iff} + $a \mathrel{\restrl{R}{X}} b$ iff $a\mathrel{R}b$ and $a\in X$. +\end{proposition} + +\begin{proposition}\label{restrl_subseteq} + $\restrl{R}{X}\subseteq R$. +\end{proposition} + +\begin{proposition}% +\label{elem_dom_of_restrl_implies_elem_dom_and_restr} + Suppose $x\in \dom{\restrl{R}{X}}$. + Then $x\in \dom{R}, X$. +\end{proposition} +\begin{proof} + Take $y$ such that $x\in X$ and $(x, y)\in \restrl{R}{X}$. + Then $(x, y)\in R$. Thus $x\in\dom{R}$. +\end{proof} + +\begin{proposition}% +\label{elem_dom_and_restr_implies_elem_of_restr} + Suppose $x\in \dom{R}, X$. + Then $x\in \dom{\restrl{R}{X}}$. +\end{proposition} +\begin{proof} + Take $y$ such that $(x, y)\in R$ by \cref{dom_iff}. + Then $(x, y)\in \restrl{R}{X}$. + Thus $x\in\dom{\restrl{R}{X}}$. +\end{proof} + +\begin{proposition}\label{restrl_eq_inter} + Suppose $R$ is a relation. + $\restrl{R}{X} = R\inter (X\times \ran{R})$. +\end{proposition} +\begin{proof} + For all $a$ we have $a\in R\inter (X\times \ran{R})$ iff $a\in \restrl{R}{X}$ + by \cref{inter,restrl,ran_iff,times_elem_is_tuple,times_tuple_intro}. + Follows by \hyperref[setext]{extensionality}. +\end{proof} + +\begin{corollary}% +\label{dom_of_restrl_eq_inter} + Suppose $R$ is a relation. + $\dom{\restrl{R}{X}} = \dom{R}\inter X$. +\end{corollary} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{restrl_restrl} + Suppose $V\subseteq U$. + Then $\restrl{\restrl{R}{U}}{V} = \restrl{R}{V}$. +\end{proposition} +\begin{proof} + For all $w$ we have $w\in\restrl{\restrl{R}{U}}{V}$ iff $w\in\restrl{R}{V}$ + by \cref{restrl,subseteq}. + Follows by \hyperref[setext]{extensionality}. +\end{proof} + +\begin{proposition}\label{restrl_by_dom} + Let $R$ be a relation. + Then $\restrl{R}{\dom{R}} = R$. +\end{proposition} +\begin{proof} + For all $w$ we have $w\in\restrl{R}{\dom{R}}$ iff $w\in R$ + by \cref{dom,restrl,relation}. + Follows by \hyperref[setext]{extensionality}. +\end{proof} + +\begin{proposition}\label{restrl_dom} + Then $\dom{\restrl{R}{X}}\subseteq X$. +\end{proposition} + +\begin{proposition}\label{restrl_ran_elim} + Suppose $X\subseteq\dom{R}$. + Let $b\in\ran{\restrl{R}{X}}$. + Then $b\in\img{R}{X}$. +\end{proposition} +\begin{proof} + Take $a\in X$ such that $(a, b)\in \restrl{R}{X}$ + by \cref{dom,ran,restrl_dom,subseteq}. + Then $a\mathrel{R} b$ and $b\in\ran{R}$. + Thus $b\in\img{R}{X}$ by \cref{img}. +\end{proof} + +\begin{proposition}\label{restrl_ran_intro} + Suppose $X\subseteq\dom{R}$. + Let $b\in\img{R}{X}$. + Then $b\in\ran{\restrl{R}{X}}$. +\end{proposition} +\begin{proof} + Follows by \cref{img,ran_intro,restrl_iff}. +\end{proof} + +\begin{proposition}\label{restrl_ran} + Suppose $X\subseteq\dom{R}$. + Then $\ran{\restrl{R}{X}} = \img{R}{X}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{restrl_img} + Suppose $X\subseteq\dom{R}$. + Then $\img{\restrl{R}{X}}{A} = \img{R}{X\inter A}$. +\end{proposition} +\begin{proof} + For all $b$ we have $b\in\img{\restrl{R}{X}}{A}$ iff $b\in \img{R}{X\inter A}$ + by \cref{restrl_iff,img_iff,inter}. + Follows by \hyperref[setext]{extensionality}. + %Follows by set extensionality. +\end{proof} + + + +\subsection{Set of relations} + +% Also called "homogeneous relation" or "endorelation". +\begin{abbreviation}\label{binary_relation_on} + $R$ is a binary relation on $X$ iff $R\subseteq X\times X$. +\end{abbreviation} + +\begin{proposition}\label{relation_subseteq_intro_elem} + Let $R$ be a relation. + Suppose $\ran{R}\subseteq B$. + Suppose $\dom{R}\subseteq A$. + Suppose $w\in R$. + Then $w\in A\times B$. +\end{proposition} +\begin{proof} + Take $a, b$ such that $(a, b) = w$. + Then $a\in\dom{R}$ and $b\in\ran{R}$. + Thus $a\in A$ and $b\in B$. + Thus $(a, b)\in A\times B$. +\end{proof} + +\begin{proposition}\label{relation_subseteq_intro} + Let $R$ be a relation. + Suppose $\ran{R}\subseteq B$. + Suppose $\dom{R}\subseteq A$. + Then $R\subseteq A\times B$. +\end{proposition} + +\begin{proposition}\label{relation_subseteq_implies_dom_subseteq_elem} + Suppose $R\subseteq A\times B$. + Suppose $a\in\dom{R}$. + Then $a\in A$. +\end{proposition} +\begin{proof} + Take $w, b$ such that $w\in R$ and $w = (a, b)$. + Follows by \cref{dom,times_tuple_elim,elem_subseteq}. +\end{proof} + +\begin{proposition}\label{relation_subseteq_implies_dom_subseteq} + Suppose $R\subseteq A\times B$. + Then $\dom{R}\subseteq A$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,relation_subseteq_implies_dom_subseteq_elem}. +\end{proof} + +\begin{proposition}\label{relation_subseteq_implies_ran_subseteq_elem} + Suppose $R\subseteq A\times B$. + Suppose $b\in\ran{R}$. + Then $b\in B$. +\end{proposition} +\begin{proof} + Take $w, a$ such that $w\in R$ and $w = (a, b)$. + Follows by \cref{ran,elem_subseteq,times_tuple_elim}. +\end{proof} + +\begin{proposition}\label{relation_subseteq_implies_ran_subseteq} + Suppose $R\subseteq A\times B$. + Then $\ran{R}\subseteq B$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,relation_subseteq_implies_ran_subseteq_elem}. +\end{proof} + +\begin{definition}\label{rels} + $\rels{A}{B} = \pow{A\times B}$. +\end{definition} + +\begin{proposition}\label{rels_intro} + Suppose $R\subseteq A\times B$. + Then $R\in\rels{A}{B}$. +\end{proposition} + +\begin{proposition}\label{rels_intro_dom_and_ran} + Let $R$ be a relation. + Suppose $\dom{R}\subseteq A$. + Suppose $\ran{R}\subseteq B$. + Then $R\in\rels{A}{B}$. +\end{proposition} +\begin{proof} + $R\subseteq A\times B$. +\end{proof} + +\begin{proposition}\label{rels_elim} + Suppose $R\in\rels{A}{B}$. + Then $R\subseteq A\times B$. +\end{proposition} + +\begin{proposition}\label{rels_dom_subseteq} + Suppose $R\in\rels{A}{B}$. + Then $\dom{R}\subseteq A$. +\end{proposition} +\begin{proof} + Follows by \cref{rels_elim,relation_subseteq_implies_dom_subseteq}. +\end{proof} + +\begin{proposition}\label{rels_ran_subseteq} + Suppose $R\in\rels{A}{B}$. + Then $\ran{R}\subseteq B$. +\end{proposition} +\begin{proof} + Follows by \cref{rels_elim,relation_subseteq_implies_ran_subseteq}. +\end{proof} + +\begin{proposition}\label{rels_is_relation} + Let $R\in\rels{A}{B}$. + Then $R$ is a relation. +\end{proposition} +\begin{proof} + It suffices to show that for all $w\in R$ there exists $x, y$ such that $w = (x, y)$. + Fix $w\in R$. + Now $R\subseteq A\times B$ by \cref{rels_elim}. + Thus $w\in A\times B$. +\end{proof} + +\begin{proposition}\label{rels_weaken_dom} + Let $R\in\rels{A}{B}$. + Suppose $A\subseteq C$. + Then $R\in\rels{C}{B}$. +\end{proposition} +\begin{proof} + $R\subseteq A\times B\subseteq C\times B$. + Thus $R\subseteq C\times B$. +\end{proof} + +\begin{proposition}\label{rels_weaken_codom} + Let $R\in\rels{A}{B}$. + Suppose $B\subseteq D$. + Then $R\in\rels{A}{D}$. +\end{proposition} +\begin{proof} + $R\subseteq A\times B\subseteq A\times D$. + Thus $R\subseteq A\times D$. +\end{proof} + +\begin{proposition}\label{rels_type} + Let $R\in\rels{A}{B}$. + Suppose $(a,b)\in R$. + Then $(a,b)\in A\times B$. +\end{proposition} +\begin{proof} + $R\subseteq A\times B$ by \cref{rels_elim}. +\end{proof} + +\begin{proposition}\label{rels_type_dom} + Let $R\in\rels{A}{B}$. + Suppose $(a,b)\in R$. + Then $a\in A$. +\end{proposition} +\begin{proof} + $(a,b)\in A\times B$ by \cref{rels_type}. +\end{proof} + +\begin{proposition}\label{rels_type_ran} + Let $R\in\rels{A}{B}$. + Suppose $(a,b)\in R$. + Then $b\in B$. +\end{proposition} +\begin{proof} + $(a,b)\in A\times B$ by \cref{rels_type}. +\end{proof} + +\begin{proposition}\label{rels_restrict_dom} + Let $R\in\rels{A}{B}$. + Then $R\in\rels{\dom{R}}{B}$. +\end{proposition} +\begin{proof} + $R$ is a relation by \cref{rels_is_relation}. + $\dom{R}\subseteq \dom{R}$ by \cref{subseteq_refl}. + $\ran{R}\subseteq B$. + Follows by \cref{rels_intro_dom_and_ran}. +\end{proof} + +\begin{proposition}\label{rels_restrict_ran} + Let $R\in\rels{A}{B}$. + Then $R\in\rels{A}{\ran{R}}$. +\end{proposition} +\begin{proof} + $R$ is a relation by \cref{rels_is_relation}. + $\dom{R}\subseteq A$. + $\ran{R}\subseteq \ran{R}$ by \cref{subseteq_refl}. + Follows by \cref{rels_intro_dom_and_ran}. +\end{proof} + +\subsection{Identity relation} + +\begin{definition}\label{id} + $\identity{A} = \{(a,a)\mid a\in A\}$. +\end{definition} + +\begin{proposition}\label{id_iff} + $a\mathrel{\identity{A}}b$ iff $a = b\in A$. +\end{proposition} +\begin{proof} + Follows by \cref{id,pair_eq_iff}. +\end{proof} + +\begin{proposition}\label{id_elem_intro} + Suppose $a\in A$. + Then $(a, a) \in\identity{A}$. +\end{proposition} +\begin{proof} + Follows by \cref{id}. +\end{proof} + +\begin{proposition}\label{id_elem_inspect} + Suppose $w\in\identity{A}$. + Then there exists $a\in A$ such that $w = (a, a)$. +\end{proposition} +\begin{proof} + Follows by \cref{id}. +\end{proof} + +\begin{proposition}\label{id_is_relation} + $\identity{A}$ is a relation. +\end{proposition} + +\begin{proposition}\label{id_dom} + $\dom{\identity{A}} = A$. +\end{proposition} +\begin{proof} + For every $a\in A$ we have $(a, a)\in \identity{A}$. + $\dom{\identity{A}} = A$ by set extensionality. +\end{proof} + +\begin{proposition}\label{id_ran} + $\ran{\identity{A}} = A$. +\end{proposition} +\begin{proof} + For every $a$ we have $a\in \ran{\identity{A}}$ iff $a\in A$ + by \cref{ran_iff,id_iff}. + For every $a\in A$ we have $(a, a)\in \identity{A}$. + $\ran{\identity{A}} = A$ by set extensionality. +\end{proof} + +\begin{proposition}\label{id_img} + $\img{\identity{A}}{B} = A\inter B$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{id_elem_rels} + $\identity{A}\in\rels{A}{A}$. +\end{proposition} + +\subsection{Membership relation} + +\begin{definition}\label{memrel} + $\memrel{A} = \{(a, b)\mid a\in A, b\in A \mid a\in b\}$. +\end{definition} + +\begin{proposition}\label{memrel_elem_intro} + Suppose $a, b\in A$. + Suppose $a\in b$. + Then $(a, b) \in\memrel{A}$. +\end{proposition} + +\begin{proposition}\label{memrel_elem_inspect} + Suppose $w\in\memrel{A}$. + Then there exists $a, b\in A$ such that $w = (a, b)$ and $a\in b$. +\end{proposition} +\begin{proof} + Follows by \cref{memrel}. +\end{proof} + +\begin{proposition}\label{memrel_is_relation} + $\memrel{A}$ is a relation. +\end{proposition} + +\subsection{Subset relation} + +\begin{definition}\label{subseteqrel} + $\subseteqrel{A} = \{(a, b)\mid a\in A, b\in A \mid a\subseteq b\}$. +\end{definition} + +\begin{proposition}\label{subseteqrel_is_relation} + $\subseteqrel{A}$ is a relation. +\end{proposition} diff --git a/library/relation/closure.tex b/library/relation/closure.tex new file mode 100644 index 0000000..8eebf08 --- /dev/null +++ b/library/relation/closure.tex @@ -0,0 +1,28 @@ +\import{relation/properties.tex} +\import{relation/equivalence.tex} + +\subsection{Closure operations on relations} + +\begin{definition}\label{reflexive_closure} + $\reflexiveClosure{X}{R} = R\union\identity{X}$. +\end{definition} + +% reflexive closure of R is the smallest reflexive relation containing R +\begin{proposition}\label{reflexive_closure_is_reflexive} + $\reflexiveClosure{X}{R}$ is reflexive on $X$. +\end{proposition} + +\begin{definition}\label{reflexive_reduction} + $\reflexiveReduction{X}{R} = R\setminus\identity{X}$. +\end{definition} + +\begin{definition}\label{symmetric_closure} + $\symmetricClosure{R} = R\union\converse{R}$. +\end{definition} + + +% LATER transitive closure + +% LATER reflexive transitive closure + +% LATER equivalence closure diff --git a/library/relation/equivalence.tex b/library/relation/equivalence.tex new file mode 100644 index 0000000..bda8486 --- /dev/null +++ b/library/relation/equivalence.tex @@ -0,0 +1,271 @@ +\import{set.tex} +\import{set/partition.tex} +\import{relation.tex} +\import{order/quasiorder.tex} + + +\subsection{Equivalences} + +% Sometimes also called "restricted equivalence". +\begin{abbreviation}\label{partialequivalence} + $E$ is a partial equivalence iff + $E$ is transitive and symmetric. +\end{abbreviation} + +\begin{proposition}\label{partialequivalence_is_quasireflexive} + Let $E$ be a partial equivalence. + Then $E$ is quasireflexive. +\end{proposition} + +\begin{abbreviation}\label{equivalence} + $E$ is an equivalence iff + $E$ is a symmetric quasiorder. +\end{abbreviation} + +\begin{abbreviation}\label{equivalence_on} + $E$ is an equivalence on $A$ iff + $E$ is a symmetric quasiorder on $A$. +\end{abbreviation} + +\begin{proposition}\label{inters_of_family_of_equivalences_is_equivalence} + Let $F$ be a family of relations. + Suppose every element of $F$ is an equivalence. + Then $\inters{F}$ is an equivalence. +\end{proposition} +\begin{proof} + $\inters{F}$ is quasireflexive by \cref{quasireflexive,inters_destr,inters_iff_forall}. + $\inters{F}$ is symmetric by \cref{symmetric,inters_iff_forall,inters_destr}. + $\inters{F}$ is transitive by \cref{transitive,inters_iff_forall,inters_destr}. +\end{proof} + +\begin{proposition}\label{inters_of_family_of_equivalences_on_a_set_is_equivalence_on_that_set} + Let $F$ be an inhabited family of relations. + Suppose every element of $F$ is an equivalence on $A$. + Then $\inters{F}$ is an equivalence on $A$. +\end{proposition} +\begin{proof} + $\inters{F}$ is reflexive on $A$ by \cref{inters_of_family_of_reflexive_relations_is_reflexive}. + $\inters{F}$ is symmetric. + $\inters{F}$ is transitive. +\end{proof} +% NOTE: the union of a family of equivalence relations is not necessarily an +% equivalence relation because a binary union of transitive relations is not +% necessarily transitive. + + +\subsubsection{Equivalence classes} + +\begin{abbreviation}\label{equiv_class} + $\equivalenceClass{E}{a} = \downward{E}{a}$. +\end{abbreviation} + +\begin{abbreviation}\label{equivclass_abbr} + The $E$-equivalence class of $a$ is $\equivalenceClass{E}{a}$. +\end{abbreviation} + +\begin{proposition}\label{equivclasses_inhabited} + Let $E$ be an equivalence. + Let $a\in \fld{E}$. + Then $a\in\equivalenceClass{E}{a}$. +\end{proposition} +\begin{proof} + $a\mathrel{E} a$ by \cref{reflexive_on,quasireflexive_implies_reflexive_on_fld}. +\end{proof} + +\begin{proposition}\label{equivclasses_inhabited_equivalenceon} + Let $E$ be an equivalence on $A$. + Let $a\in A$. + Then $a\in\equivalenceClass{E}{a}$. +\end{proposition} +\begin{proof} + $a\mathrel{E} a$ by \cref{reflexive_on}. +\end{proof} + +\begin{proposition}\label{equiv_implies_equivanlence_classes_eq} + Let $E$ be an equivalence on $A$. + Let $a, b\in A$. + Suppose $a\mathrel{E} b$. + Then $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{equivclasses_eq_implies_equiv} + Let $E$ be an equivalence on $A$. + Let $a, b\in A$. + Suppose $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$. + Then $a\mathrel{E} b$. +\end{proposition} + +\begin{proposition}\label{equiv_iff_equivclasses_eq} + Let $E$ be an equivalence on $A$. + Let $a, b\in A$. + Then $a\mathrel{E} b$ iff $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$. +\end{proposition} + +\begin{proposition}\label{equivclasses_diseq_implies_disjoint} + Let $E$ be a partial equivalence. + Suppose $\equivalenceClass{E}{a}\neq \equivalenceClass{E}{b}$. + Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$. +\end{proposition} +\begin{proof} + Suppose not. + Take $c$ such that $c\in \equivalenceClass{E}{a},\equivalenceClass{E}{b}$. + Then $c\mathrel{E} a$ and + $c\mathrel{E} b$. + $E$ is symmetric. + Thus $a\mathrel{E} c$ by \hyperref[symmetric]{symmetry}. + $E$ is transitive. + Thus $a\mathrel{E} b$ by \hyperref[transitive]{transitivity}. + Then $b\mathrel{E} a$ by \hyperref[symmetric]{symmetry}. + % + Thus $a\in \equivalenceClass{E}{b}$ and $b\in \equivalenceClass{E}{a}$ + by \cref{downward_closure_iff}. + Hence $\equivalenceClass{E}{a}\subseteq \equivalenceClass{E}{b}\subseteq \equivalenceClass{E}{a}$ + by \cref{transitive_downward_subseteq}. + Contradiction by \cref{subseteq_antisymmetric}. +\end{proof} + +\begin{corollary}\label{equivalence_equivclasses_diseq_implies_disjoint} + Let $E$ be an equivalence. + Suppose $\equivalenceClass{E}{a}\neq \equivalenceClass{E}{b}$. + Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$. +\end{corollary} +\begin{proof} + Follows by \cref{equivclasses_diseq_implies_disjoint}. +\end{proof} + +\begin{corollary}\label{equivalenceon_equivclasses_diseq_implies_disjoint} + Let $E$ be an equivalence on $A$. + Suppose $\equivalenceClass{E}{a}\neq \equivalenceClass{E}{b}$. + Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$. +\end{corollary} +\begin{proof} + Follows by \cref{equivclasses_diseq_implies_disjoint}. +\end{proof} + + +\subsubsection{Quotients} + +\begin{definition}\label{quotient} + $\quotient{A}{E} = \{\equivalenceClass{E}{a}\mid a\in A\}$. +\end{definition} + +%\begin{definition}\label{equivalenceclasses} +% $\equivalenceClasses{E} = \{\equivalenceClass{E}{a}\mid a\in\dom{E}\}$. +%\end{definition} + +\begin{proposition}\label{quotient_emptyset} + $\quotient{\emptyset}{\emptyset} = \emptyset$. +\end{proposition} + + +\begin{proposition}\label{quotient_elems_disjoint} + Let $E$ be an equivalence on $A$. + Suppose $B,C\in\quotient{A}{E}$ and $B\neq C$. + Then $B$ is disjoint from $C$. +\end{proposition} +\begin{proof} + Take $b$ such that $B = \equivalenceClass{E}{b}$. + Take $c$ such that $C = \equivalenceClass{E}{c}$. + Then $B$ is disjoint from $C$ by \cref{equivalenceon_equivclasses_diseq_implies_disjoint}. +\end{proof} + +\begin{proposition}\label{quotient_elems_inhabited} + Let $E$ be an equivalence on $A$. + Suppose $C\in\quotient{A}{E}$. + Then $C$ is inhabited. +\end{proposition} +\begin{proof} + Take $a\in A$ such that $C = \equivalenceClass{E}{a}$. + Then $a\in \equivalenceClass{E}{a}$. + $C$ is inhabited by \cref{quotient,inhabited,equivclasses_inhabited}. +\end{proof} + +\begin{proposition}\label{quotient_elems_type} + Let $E$ be an equivalence on $A$. + Suppose $a\in C\in\quotient{A}{E}$. + Then $a\in A$. +\end{proposition} +\begin{proof} + Take $b\in A$ such that $C = \equivalenceClass{E}{b}$ + by \cref{quotient}. + Then $a\mathrel{E} b$. + Thus $a\in A$ by \cref{times_tuple_elim,subseteq}. +\end{proof} + + +\begin{corollary}\label{quotient_notni_emptyset} + Let $E$ be an equivalence on $A$. + $\emptyset\notin\quotient{A}{E}$. +\end{corollary} + +\begin{proposition}\label{quotient_partition} + Let $E$ be an equivalence on $A$. + $\quotient{A}{E}$ is a partition. +\end{proposition} +\begin{proof} + $\emptyset\notin\quotient{A}{E}$. + For all $B, C\in \quotient{A}{E}$ such that $B\neq C$ we have $B$ is disjoint from $C$. +\end{proof} + +\begin{proposition}\label{quotient_partition_of} + Let $E$ be an equivalence on $A$. + $\quotient{A}{E}$ is a partition of $A$. +\end{proposition} +\begin{proof} + $\unions{(\quotient{A}{E})} = A$ by set extensionality. +\end{proof} + + + +\begin{definition}\label{equivalence_from_partition} + $\equivfrompartition{P} = \{(a, b)\mid a\in A, b\in A\mid \exists C\in P.\ a, b\in C\}$. +\end{definition} + +\begin{proposition}\label{equivalence_from_partition_intro} + Let $P$ be a partition of $A$. + Let $a,b\in A$. + Suppose $a,b\in C\in P$. + Then $a\mathrel{\equivfrompartition{P}} b$. +\end{proposition} + +\begin{proposition}\label{equivalence_from_partition_reflexive} + Let $P$ be a partition of $A$. + $\equivfrompartition{P}$ is reflexive on $A$. +\end{proposition} + +\begin{proposition}\label{equivalence_from_partition_symmetric} + Let $P$ be a partition. + $\equivfrompartition{P}$ is symmetric. +\end{proposition} +\begin{proof} + Follows by \cref{symmetric,equivalence_from_partition,notin_emptyset}. +\end{proof} + +\begin{proposition}\label{equivalence_from_partition_transitive} + Let $P$ be a partition. + $\equivfrompartition{P}$ is transitive. +\end{proposition} + +\begin{proposition}\label{equivalence_from_partition_is_equivalence} + Let $P$ be a partition of $A$. + $\equivfrompartition{P}$ is an equivalence on $A$. +\end{proposition} + +\begin{proposition}\label{equivalence_from_quotient} + Let $E$ be an equivalence on $A$. + Then $\equivfrompartition{\quotient{A}{E}} = E$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{partition_eq_quotient_by_equivalence_from_partition} + Let $P$ be a partition of $A$. + Then $\quotient{A}{\equivfrompartition{P}} = P$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} diff --git a/library/relation/properties.tex b/library/relation/properties.tex new file mode 100644 index 0000000..191b7c0 --- /dev/null +++ b/library/relation/properties.tex @@ -0,0 +1,202 @@ +\import{set.tex} +\import{relation.tex} + +\subsection{Properties of relations} + +\begin{definition}\label{left_quasireflexive} + $R$ is left quasireflexive iff + for all $x, y$ such that $x\mathrel{R} y$ + we have $x\mathrel{R}x$. +\end{definition} + +\begin{definition}\label{right_quasireflexive} + $R$ is right quasireflexive iff + for all $x, y$ such that $x\mathrel{R} y$ + we have $y\mathrel{R}y$. +\end{definition} + +\begin{definition}\label{quasireflexive} + $R$ is quasireflexive iff + for all $x, y$ such that $x\mathrel{R} y$ + we have $x\mathrel{R}x$ and $y\mathrel{R}y$. +\end{definition} + +\begin{definition}\label{coreflexive} + $R$ is coreflexive iff + for all $x, y$ such that $x\mathrel{R} y$ + we have $x = y$. +\end{definition} + +\begin{definition}\label{reflexive_on} + $R$ is reflexive on $X$ iff + for all $x\in X$ + we have $x\mathrel{R}x$. +\end{definition} + +\begin{definition}\label{irreflexive} + $R$ is irreflexive iff + for all $x$ we have $(x,x)\notin R$. +\end{definition} + + +\begin{proposition}\label{quasireflexive_implies_reflexive_on_fld} + Suppose $R$ is quasireflexive. + Then $R$ is reflexive on $\fld{R}$. +\end{proposition} + +\begin{proposition}\label{reflexive_on_fld_impliesquasireflexive} + Suppose $R$ is reflexive on $\fld{R}$. + Then $R$ is quasireflexive. +\end{proposition} + +\begin{proposition}\label{inters_of_family_of_reflexive_relations_is_reflexive} + Let $F$ be an inhabited family of relations. + Suppose every element of $F$ is reflexive on $A$. + Then $\inters{F}$ is reflexive on $A$. +\end{proposition} +\begin{proof} + For all $a\in A$ we have for all $R\in F$ we have $a\mathrel{R} a$. + Thus for all $a\in A$ we have $a\mathrel{(\inters{F})} a$. +\end{proof} + +\begin{definition}\label{antisymmetric} + $R$ is antisymmetric iff + for all $x, y$ such that $x\mathrel{R}y\mathrel{R}x$ + we have $x = y$. +\end{definition} + +\begin{definition}[Symmetry]\label{symmetric} + $R$ is symmetric iff + for all $x, y$ we have + $x\mathrel{R} y \iff y\mathrel{R}x$. +\end{definition} + +\begin{definition}\label{asymmetric} + $R$ is asymmetric iff + for all $x, y$ such that + $x\mathrel{R} y$ we have $y\not\mathrel{R}x$. +\end{definition} + +\begin{proposition}\label{asymmetric_implies_irreflexive} + Suppose $R$ is asymmetric. + Then $R$ is irreflexive. +\end{proposition} + +\begin{proposition}\label{asymmetric_implies_antisymmetric} + Suppose $R$ is asymmetric. + Then $R$ is antisymmetric. +\end{proposition} + +\begin{proposition}\label{antisymmetric_and_irreflexive_implies_asymmetric} + Suppose $R$ is antisymmetric. + Suppose $R$ is irreflexive. + Then $R$ is asymmetric. +\end{proposition} + +% TODO +%\begin{proposition}\label{symmetric_relation_eq_converse} +% Let $R$ be a symmetric relation. +% Then $\converse{R} = R$. +%\end{proposition} +%\begin{proof} +% Follows by set extensionality. +%\end{proof} + +\begin{definition}[Transitivity]\label{transitive} + $R$ is transitive iff + for all $x, y, z$ such that $x\mathrel{R}y\mathrel{R}z$ + we have $x\mathrel{R} z$. +\end{definition} + +\begin{proposition}\label{transitive_downward_elem} + Suppose $R$ is transitive. + Suppose $a\in\downward{R}{b}$. + Suppose $c\in\downward{R}{a}$. + Then $c\in \downward{R}{b}$. +\end{proposition} +\begin{proof} + $c\mathrel{R} a\mathrel{R}b$. + Thus $c\mathrel{R} b$ by \hyperref[transitive]{transitivity}. +\end{proof} + +\begin{proposition}\label{transitive_downward_subseteq} + Suppose $R$ is transitive. + Suppose $a\in\downward{R}{b}$. + Then $\downward{R}{a}\subseteq \downward{R}{b}$. +\end{proposition} + +\begin{definition}\label{dense} + $R$ is dense iff + for all $x, z$ such that $x\mathrel{R}z$ + there exists $y$ such that $x\mathrel{R}y\mathrel{R}z$. +\end{definition} + +% Variation of connexity that does not depend on a carrier. +\begin{definition}\label{quasiconnex} + $R$ is quasiconnex iff + for all $x, y\in\fld{R}$ such that $x\neq y$ we have + $x\mathrel{R}y$ or $y\mathrel{R}x$. +\end{definition} + +% Also called "connected" (here reserved for topology), +% "complete" (heavily overloaded), and total" (also overloaded). +\begin{definition}\label{connex} + $R$ is connex on $X$ iff + for all $x, y\in X$ such that $x\neq y$ we have + $x\mathrel{R}y$ or $y\mathrel{R}x$. +\end{definition} + +\begin{definition}\label{strongly_quasiconnex} + $R$ is strongly quasiconnex iff + for all $x, y\in\fld{R}$ we have + $x\mathrel{R}y$ or $y\mathrel{R}x$. +\end{definition} + +\begin{definition}\label{strongly_connex} + $R$ is strongly connex on $X$ iff + for all $x, y\in X$ we have + $x\mathrel{R}y$ or $y\mathrel{R}x$. +\end{definition} + +%\begin{proposition}\label{strongly_quasiconnex_implies_quasiconnex_and_quasireflexive} +% Suppose $R$ is strongly quasiconnex. +% Then $R$ is quasiconnex and quasireflexive. +%\end{proposition} + +%\begin{proposition}\label{quasiconnex_and_quasireflexive_implies_strongly_quasiconnex} +% Suppose $R$ is quasiconnex and quasireflexive. +% Then $R$ is strongly quasiconnex. +%\end{proposition} + +\begin{proposition}\label{strongly_quasiconnex_iff_quasiconnex_and_quasireflexive} + $R$ is strongly quasiconnex iff + $R$ is quasiconnex and quasireflexive. +\end{proposition} +\begin{proof} + Follows by \cref{quasiconnex,strongly_quasiconnex,quasireflexive_implies_reflexive_on_fld,reflexive_on,fld,reflexive_on_fld_impliesquasireflexive}. +\end{proof} + +\begin{proposition}\label{connex_reaches_all_or_all_but_one} + Suppose $R$ is connex on $A$. + Let $a, b\in A\setminus\ran{R}$. + Then $a = b$. +\end{proposition} +\begin{proof} + Suppose not. + $a, b\in A$. + Then $(a, b)\in R$ or $(b,a)\in R$ by \cref{connex}. + $(a, b)\notin R$. + $(b, a)\notin R$. + Thus $a = b$. +\end{proof} + + +\begin{definition}\label{righteuclidean} + $R$ is right Euclidean iff + for all $a,b,c$ such that $a\mathrel{R}b,c$ we have $b\mathrel{R}c$. +\end{definition} + +\begin{definition}\label{lefteuclidean} + $R$ is left Euclidean iff + for all $a,b,c$ such that $a,b\mathrel{R}c$ we have $a\mathrel{R}b$. +\end{definition} diff --git a/library/relation/uniqueness.tex b/library/relation/uniqueness.tex new file mode 100644 index 0000000..68b01de --- /dev/null +++ b/library/relation/uniqueness.tex @@ -0,0 +1,81 @@ +\import{set.tex} +\import{relation.tex} + + +\subsection{Injective relations} + +% Injective relations are also called "left-unique" +\begin{definition}\label{injective} + $R$ is injective iff for all $a,a',b$ such that $a, a'\mathrel{R} b$ we have $a = a'$. +\end{definition} + +\begin{abbreviation}\label{leftunique} + $R$ is left-unique iff $R$ is injective. +\end{abbreviation} + +\begin{proposition}\label{subseteq_of_injective_is_injective} + Suppose $S\subseteq R$. + Suppose $R$ is injective. + Then $S$ is injective. +\end{proposition} + +\begin{proposition}\label{restrl_injective} + Suppose $R$ is injective. + Then $\restrl{R}{A}$ is injective. +\end{proposition} +\begin{proof} + $\restrl{R}{A}\subseteq R$. +\end{proof} + +\begin{proposition}\label{circ_injective} + Suppose $R$ and $S$ are injective. + Then $S\circ R$ is injective. +\end{proposition} + +\begin{proposition}\label{identity_injective} + Then $\identity{A}$ is injective. +\end{proposition} + +\subsection{Right-unique relations} + +% also called "functional" or "univalent" +\begin{definition}\label{rightunique} + $R$ is right-unique iff + for all $a,b,b'$ such that $a\mathrel{R} b, b'$ we have $b = b'$. +\end{definition} + +\begin{abbreviation}\label{onetoone} + $R$ is one-to-one iff $R$ is right-unique and injective. +\end{abbreviation} + +\begin{proposition}\label{subseteq_of_rightunique_is_rightunique} + Suppose $S\subseteq R$. + Suppose $R$ is right-unique. + Then $S$ is right-unique. +\end{proposition} + +\begin{proposition}\label{circ_rightunique} + Suppose $R$ and $S$ are right-unique. + Then $S\circ R$ is right-unique. +\end{proposition} + + + +\subsection{Left-total relations} + +\begin{definition}\label{lefttotal} + $R$ is left-total on $A$ iff + for all $a\in A$ there exists $b$ such that $a\mathrel{R} b$. +\end{definition} + + +\subsection{Right-total relations} + +\begin{definition}\label{righttotal} + $R$ is right-total on $B$ iff + for all $b\in B$ there exists $a$ such that $a\mathrel{R} b$. +\end{definition} + +\begin{abbreviation}\label{surjective} + $R$ is surjective on $B$ iff $R$ is right-total on $B$. +\end{abbreviation} diff --git a/library/set.tex b/library/set.tex new file mode 100644 index 0000000..33e5af4 --- /dev/null +++ b/library/set.tex @@ -0,0 +1,968 @@ +\section{Sets} + +\begin{abbreviation}\label{ni} + $A\ni a$ iff $a\in A$. +\end{abbreviation} + +\subsection{Extensionality} + +The axiom of set extensionality says that sets are determined by their \textit{extension}, +that is, two sets are equal iff they have the same elements. +% +\begin{axiom}[Set extensionality]\label{setext} + Suppose for all $a$ we have $a\in A$ iff $a\in B$. + Then $A = B$. +\end{axiom} + +This axiom is also available as the justification “{\ldots\ by set extensionality}”, +which applies it to goals of the form “$A = B$” and “$A \neq B$”. + +\begin{proposition}[Witness for disequality]% +\label{neq_witness} + Suppose $A\neq B$. + Then there exists $c$ such that + either $c\in A$ and $c\not\in B$ + or $c\not\in A$ and $c\in B$. +\end{proposition} +\begin{proof} + Suppose not. Then $A = B$ by set extensionality. Contradiction. +\end{proof} + + + +\subsection{Subsets} + +\begin{definition}\label{subseteq} + $A\subseteq B$ iff + for all $a\in A$ we have $a\in B$. +\end{definition} + +\begin{abbreviation}\label{is_subset} + $A$ is a subset of $B$ iff $A\subseteq B$. +\end{abbreviation} + +\begin{abbreviation}\label{supseteq} + $B\supseteq A$ iff $A\subseteq B$. +\end{abbreviation} + +\begin{proposition}% +\label{subseteq_refl} + $A\subseteq A$. +\end{proposition} + +\begin{proposition}% +\label{subseteq_antisymmetric} + Suppose $A\subseteq B\subseteq A$. + Then $A = B$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{elem_subseteq} + Suppose $a\in A\subseteq B$. + Then $a\in B$. +\end{proposition} + +\begin{proposition}% +\label{not_in_subseteq} + Suppose $A\subseteq B$ and $c\notin B$. + Then $c\notin A$. +\end{proposition} + +\begin{proposition}% +\label{subseteq_transitive} + Suppose $A\subseteq B\subseteq C$. + Then $A\subseteq C$. +\end{proposition} + +\begin{definition}\label{subset} + $A\subset B$ iff + $A\subseteq B$ and $A\neq B$. +\end{definition} + +\begin{proposition}\label{subset_irrefl} + $A\not\subset A$. +\end{proposition} + +\begin{proposition}\label{subset_transitive} + Suppose $A\subseteq B\subseteq C$. + Then $A\subseteq C$. +\end{proposition} + +\begin{proposition}\label{subset_witness} + Suppose $A\subset B$. + Then there exists $b\in B$ such that $b\notin A$. +\end{proposition} +\begin{proof} + $A\subseteq B$ and $A\neq B$. +\end{proof} + +\begin{abbreviation}\label{family_of_subsets} + $F$ is a family of subsets of $X$ iff + for all $A\in F$ we have $A\subseteq X$. +\end{abbreviation} + + +\subsection{The empty set} + +\begin{axiom}% +\label{notin_emptyset} + For all $a$ we have $a\notin\emptyset$. +\end{axiom} + +\begin{definition}\label{inhabited} + $A$ is inhabited iff + there exists $a$ such that $a\in A$. +\end{definition} + +\begin{abbreviation}\label{empty} + $A$ is empty iff $A$ is not inhabited. +\end{abbreviation} + +%\begin{proposition}% +%\label{inhabited_iff_nonempty} +% $A$ is inhabited iff $A$ is not empty. +%\end{proposition} + +\begin{proposition}% +\label{empty_eq} + If $x$ and $y$ are empty, then $x = y$. +\end{proposition} + +\begin{proposition}% +\label{emptyset_subseteq} + For all $a$ we have $\emptyset \subseteq a$. + % LATER $\emptyset$ is a subset of every set. +\end{proposition} + +\begin{proposition}% +\label{subseteq_emptyset_iff} + $A\subseteq \emptyset$ iff $A = \emptyset$. +\end{proposition} + + +\subsection{Disjointness of sets} + +\begin{definition}\label{disjoint} + $A$ is disjoint from $B$ iff there exists no $a$ such that $a\in A, B$. +\end{definition} + +\begin{abbreviation}\label{notmeets} + $A\notmeets B$ iff $A$ is disjoint from $B$. +\end{abbreviation} + +\begin{abbreviation}\label{meets} + $A\meets B$ iff $A$ is not disjoint from $B$. +\end{abbreviation} + +\begin{proposition}% +\label{disjoint_symmetric} + If $A$ is disjoint from $B$, then $B$ is disjoint from $A$. +\end{proposition} + + + + + +\subsection{Unordered pairing and set adjunction} + +Finite set expressions are desugared to +iterated application of $\operatorname{\textsf{cons}}$ to $\emptyset$. +Thus $\{x,y,z\}$ is an abbreviaton of +$\cons{x}{\cons{y}{\cons{z}{\emptyset}}}$. +The $\operatorname{\textsf{cons}}$ operation is determined by the following axiom: +% +\begin{axiom}\label{cons_iff} + $x\in \cons{y}{X}$ iff $x = y$ or $x\in X$. +\end{axiom} + +\begin{proposition}\label{cons_left} + $x\in \cons{x}{X}$. +\end{proposition} + +\begin{proposition}\label{cons_right} + If $y\in X$, then $y\in \cons{x}{X}$. +\end{proposition} + + +% Unordered pairs: + +\begin{proposition}\label{upair_intro_left} + $a\in\{a,b\}$. +\end{proposition} + +\begin{proposition}\label{upair_intro_right} + $b\in\{a,b\}$. +\end{proposition} + +\begin{proposition}\label{upair_elim} + Suppose $c\in\{a,b\}$. Then $a = c$ or $b = c$. +\end{proposition} + +\begin{proposition}\label{upair_iff} + $c\in\{a,b\}$ iff $a = c$ or $b = c$. +\end{proposition} + + +% Singletons: + +\begin{proposition}\label{singleton_intro} + $a\in\{a\}$. +\end{proposition} + +\begin{proposition}\label{singleton_elim} + If $a\in\{b\}$, then $a = b$. +\end{proposition} + +\begin{proposition}\label{singleton_iff} + $a\in\{b\}$ iff $a = b$. +\end{proposition} + +\begin{abbreviation}\label{subsingleton} + $A$ is a subsingleton iff for all $a, b\in A$ we have $a = b$. +\end{abbreviation} + +\begin{proposition}\label{singleton_inhabited} + $\{a\}$ is inhabited. +\end{proposition} + +\begin{proposition}\label{singleton_iff_inhabited_subsingleton} + Let $A$ be a subsingleton. + Let $a\in A$. + Then $A = \{a\}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{singleton_subset_intro} + Suppose $a\in C$. + Then $\{a\}\subseteq C$. +\end{proposition} + +\begin{proposition}\label{singleton_subset_elim} + Suppose $\{a\}\subseteq C$. + Then $a\in C$. +\end{proposition} + + +\subsection{Union and intersection} + +\subsubsection{Union of a set} + +\begin{axiom}\label{unions_iff} + $z\in\unions{X}$ iff there exists $Y\in X$ such that $z\in Y$. +\end{axiom} + + +\begin{proposition}% +\label{unions_intro} + Suppose $A\in B\in C$. + Then $A\in\unions{C}$. +\end{proposition} +\begin{proof} + There exists $B\in C$ such that $A\in B$. +\end{proof} + +\begin{proposition}% +\label{unions_emptyset} + $\unions{\emptyset} = \emptyset$. +\end{proposition} + +\begin{proposition}\label{unions_family} + Let $F$ be a family of subsets of $X$. + Then $\unions{F}\subseteq X$. +\end{proposition} + +\begin{abbreviation}\label{closedunderunions} + $T$ is closed under arbitrary unions + iff for every subset $M$ of $T$ we have $\unions{M}\in T$. +\end{abbreviation} + +\subsubsection{Intersection of a set} + +\begin{definition}\label{inters} + $\inters{A} = \{ x\in\unions{A}\mid \text{for all $a\in A$ we have $x\in a$} \}$. +\end{definition} + +\begin{proposition}\label{inters_iff_forall} + $z\in\inters{X}$ iff $X$ is inhabited and for all $Y\in X$ we have $z\in Y$. +\end{proposition} + +\begin{proposition}% +\label{inters_intro} + Suppose $C$ is inhabited. + Suppose for all $B\in C$ we have $A\in B$. + Then $A\in\inters{C}$. +\end{proposition} + +\begin{proposition}\label{inters_destr} + Suppose $A\in\inters{C}$. + Suppose $B\in C$. + Then $A\in B$. +\end{proposition} + +\begin{proposition}\label{inters_greatest} + Suppose $A$ is inhabited. + Suppose for all $a\in A$ we have $C\subseteq a$. + Then $C\subseteq\inters{A}$. +\end{proposition} + +\begin{proposition}\label{subseteq_inters_iff} + Suppose $A$ is inhabited. + Then $C\subseteq\inters{A}$ iff for all $a\in A$ we have $C\subseteq a$. +\end{proposition} + +\begin{proposition}\label{inters_subseteq_elem} + Let $B\in A$. + Then $\inters{A}\subseteq B$. +\end{proposition} + +\begin{proposition}\label{inters_singleton} + $\inters{\{a\}} = a$. +\end{proposition} +\begin{proof} + Every element of $a$ is an element of $\inters{\{a\}}$ + by \cref{inters_iff_forall,singleton_iff,singleton_inhabited}. + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{inters_emptyset} + $\inters{\{\emptyset\}} = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\subsubsection{Binary union} + +\begin{axiom}\label{union_iff} + Let $A, B$ be sets. + $a\in A\union B$ iff $a\in A$ or $a\in B$. +\end{axiom} + +\begin{proposition}\label{union_intro_left} + If $c\in A$, then $c\in A\union B$. +\end{proposition} + +\begin{proposition}\label{union_intro_right} + If $c\in B$, then $c\in A\union B$. +\end{proposition} + +\begin{proposition}\label{union_as_unions} + $\unions{\{x,y\}} = x\union y$. +\end{proposition} +\begin{proof} + %For all z we have + %\begin{align*} + % z\in \unions{\{x,y\}} + % &\iff \exists Z\in\{x,y\}. z\in Z + %\end{align*} + Follows by set extensionality. +\end{proof} + +\begin{proposition}[Commutativity of union]% +\label{union_comm} + $A\union B = B\union A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}[Associativity of union]% +\label{union_assoc} + $(A\union B)\union C = A\union (B\union C)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}[Idempotence of union]% +\label{union_idempotent} + $A\union A = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{subseteq_union_iff} + $A\union B\subseteq C$ iff $A\subseteq C$ and $B\subseteq C$. +\end{proposition} + +\begin{proposition}\label{union_upper_left} + $A\subseteq A\union B$. +\end{proposition} + +\begin{proposition}\label{union_upper_right} + $B\subseteq A\union B$. +\end{proposition} + +\begin{proposition}\label{union_subseteq_union} + Suppose $A\subseteq C$ and $B\subseteq D$. + Then $A\union B\subseteq C\union D$. +\end{proposition} + +\begin{proposition}% +\label{union_emptyset} + $A\union\emptyset = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + + +\begin{proposition}% +\label{union_emptyset_intro} + Suppose $A = \emptyset$ and $B = \emptyset$. Then $A\union B = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{union_emptyset_elim_left} + Suppose $A\union B = \emptyset$. Then $A = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{union_emptyset_elim_right} + Suppose $A\union B = \emptyset$. Then $B = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{union_absorb_subseteq_left} + Suppose $A\subseteq B$. Then $A\union B = B$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{union_absorb_subseteq_right} + Suppose $A\subseteq B$. Then $B\union A = B$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{union_eq_self_implies_subseteq} + If $A\union B = B$, then $A\subseteq B$. +\end{proposition} + +\begin{proposition}\label{unions_cons} + $\unions{\cons{b}{A}} = b\union\unions{A}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_cons} + $\cons{b}{A} \union C = \cons{b}{A\union C}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_absorb_left} + $A\union (A\union B) = A\union B$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_absorb_right} + $(A\union B)\union B = A\union B$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_comm_left} + $A\union (B\union C) = B\union (A\union C)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{abbreviation}\label{closedunderunion} + $T$ is closed under binary unions + iff for every $U,V\in T$ we have $U\union V\in T$. +\end{abbreviation} + + +\subsubsection{Binary intersection} + +\begin{definition}\label{inter} + $A\inter B = \{ a \in A \mid a\in B\}$. +\end{definition} + +\begin{proposition}\label{inter_intro} + If $c\in A, B$, then $c\in A\inter B$. +\end{proposition} + +\begin{proposition}\label{inter_elim_left} + If $c\in A\inter B$, then $c\in A$. +\end{proposition} + +\begin{proposition}\label{inter_elim_right} + If $c\in A\inter B$, then $c\in B$. +\end{proposition} + +\begin{proposition}\label{inter_as_inters} + $\inters{\{A,B\}} = A\inter B$. +\end{proposition} +\begin{proof} + $\{A,B\}$ is inhabited. + Thus for all $c$ we have $c\in\inters{\{A,B\}}$ iff $c\in A\inter B$ + by \cref{inters_iff_forall,inter,upair_iff}. + %Thus $\inters{\{A,B\}} = A\inter B$ by \hyperref[setext]{extensionality}. + Follows by \hyperref[setext]{extensionality}. +\end{proof} + + +\begin{proposition}[Commutativity of intersection]% +\label{inter_comm} + $A\inter B = B\inter A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}[Associativity of intersection]% +\label{inter_assoc} + $(A\inter B)\inter C = A\inter (B\inter C)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}[Idempotence of intersection]% +\label{inter_idempotent} + $A\inter A = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{inter_subseteq} + $A\inter B\subseteq A$. +\end{proposition} + +\begin{proposition}% +\label{inter_emptyset} + $A\inter\emptyset = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{inter_absorb_supseteq_right} + Suppose $A\subseteq B$. Then $A\inter B = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{inter_absorb_supseteq_left} + Suppose $A\subseteq B$. Then $B\inter A = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{inter_eq_left_implies_subseteq} + Suppose $A\inter B = A$. Then $A\subseteq B$. +\end{proposition} + +\begin{proposition}% +\label{subseteq_inter_iff} + $C\subseteq A\inter B$ iff $C\subseteq A$ and $C\subseteq B$. +\end{proposition} + +\begin{proposition}% +\label{inter_lower_left} + $A\inter B \subseteq A$. +\end{proposition} + +\begin{proposition}% +\label{inter_lower_right} + $A\inter B \subseteq B$. +\end{proposition} + +\begin{proposition}\label{inter_absorb_left} + $A\inter (A\inter B) = A\inter B$. +\end{proposition} +\begin{proof} Follows by set extensionality. \end{proof} + +\begin{proposition}% +\label{inter_absorb_right} + $(A\inter B) \inter B = A\inter B$. +\end{proposition} +\begin{proof} Follows by set extensionality. \end{proof} + +\begin{proposition}\label{inter_comm_left} + $A\inter (B\inter C) = B\inter (A\inter C)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{abbreviation}\label{closedunderinter} + $T$ is closed under binary intersections + iff for every $U,V\in T$ we have $U\inter V\in T$. +\end{abbreviation} + +\subsubsection{Interaction of union and intersection} + +\begin{proposition}[Binary intersection over binary union]% +\label{inter_distrib_union} + $x\inter (y\union z) = (x\inter y)\union (x\inter z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}[Binary union over binary intersection]% +\label{union_distrib_inter} + $x\union (y\inter z) = (x\union y)\inter (x\union z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +% Halmos, Naive Set Theory, page 16 +\begin{proposition}\label{union_inter_assoc_intro} + Suppose $C\subseteq A$. + Then $(A\inter B)\union C = A\inter (B\union C)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +% Halmos, Naive Set Theory, page 16 +\begin{proposition}\label{union_inter_assoc_elim} + Suppose $(A\inter B)\union C = A\inter (B\union C)$. + Then $C\subseteq A$. +\end{proposition} + +% From Isabelle/ZF equalities theory +\begin{proposition}\label{union_inter_crazy} + $(A\inter B)\union (B\inter C)\union (C\inter A) + = + (A\union B)\inter (B\union C)\inter (C\union A)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + + +\begin{proposition}[Intersection over binary union]\label{inters_distrib_union} + Suppose $A$ and $B$ are inhabited. + Then $\inters{A\union B} = (\inters{A})\inter\inters{B}$. +\end{proposition} +\begin{proof} + $A\union B$ is inhabited. + Thus for all $c$ we have $c\in\inters{A\union B}$ iff $c\in(\inters{A})\inter\inters{B}$ + by \cref{inter,union_iff,inters_iff_forall}. + Follows by \hyperref[setext]{set extensionality}. % We only need the actual setext axiom here, not the tactic. +\end{proof} + +\subsection{Set difference} + +\begin{definition}\label{setminus} + $A\setminus B = \{ a \in A \mid a\not\in B\}$. +\end{definition} + +\begin{proposition}\label{setminus_intro} + If $a\in A$ and $a\notin B$, then $a\in A\setminus B$. +\end{proposition} + +\begin{proposition}\label{setminus_elim_left} + If $a\in A\setminus B$, then $a\in A$. +\end{proposition} + +\begin{proposition}\label{setminus_elim_right} + If $a\in A\setminus B$, then $a\notin B$. +\end{proposition} + +\begin{proposition}\label{setminus_emptyset} + $x\setminus \emptyset = x$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{emptyset_setminus} + $\emptyset\setminus x = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{setminus_self} + $x\setminus x = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +% NOTE: This theorem tends to show up spuriously in ATP proofs! +% Getting rid of it via explicit \cref{..} can save time. +\begin{proposition}\label{setminus_setminus} + $x\setminus (x\setminus y) = x\inter y$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{double_relative_complement} + Suppose $y\subseteq x$. + $x\setminus (x\setminus y) = y$. +\end{proposition} +\begin{proof} + Follows by \cref{setminus_setminus,inter_absorb_supseteq_left}. +\end{proof} + +\begin{proposition}\label{setminus_inter} + $x\setminus (y\inter z) = (x\setminus y)\union (x\setminus z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{setminus_union} + $x\setminus (y\union z) = (x\setminus y)\inter (x\setminus z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{inter_setminus} + $x\inter (y\setminus z) = (x\inter y)\setminus (x\inter z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{difference_with_proper_subset_is_inhabited} + Let $A, B$ be sets. + Suppose $A\subset B$. + Then $B\setminus A$ is inhabited. +\end{proposition} +\begin{proof} + Take $b$ such that $b\in B$ and $b\notin A$. + Then $b\in B\setminus A$. +\end{proof} + +\begin{proposition}\label{setminus_subseteq} + $B\setminus A\subseteq B$. +\end{proposition} + +\begin{proposition}\label{subseteq_setminus} + Suppose $C\subseteq A$. + Suppose $C\inter B = \emptyset$. + Then $C\subseteq A\setminus B$. +\end{proposition} + + +\begin{proposition}\label{subseteq_implies_setminus_supseteq} + Suppose $A\subseteq B$. + Then $C\setminus A\supseteq C\setminus B$. +\end{proposition} + +\begin{proposition}\label{setminus_absorb_right} + Suppose $A\inter B = \emptyset$. + Then $A\setminus B = A$. +\end{proposition} + +\begin{proposition}\label{setminus_eq_emptyset_iff_subseteq} + $A\setminus B = \emptyset$ iff $A\subseteq B$. +\end{proposition} + +\begin{proposition}\label{subseteq_setminus_cons_intro} + Suppose $B\subseteq A\setminus C$ and $c\notin B$. Then $B\subseteq A\setminus\cons{c}{C}$. +\end{proposition} + +\begin{proposition}\label{subseteq_setminus_cons_elim} + Suppose $B\subseteq A\setminus\cons{c}{C}$. Then $B\subseteq A\setminus C$ and $c\notin B$. +\end{proposition} + +\begin{proposition}\label{setminus_cons} + $A\setminus \cons{a}{B} = (A\setminus \{a\})\setminus B$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} +\begin{proposition}\label{setminus_cons_flip} + $A\setminus \cons{a}{B} = (A\setminus B)\setminus \{a\}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{setminus_disjoint} + $A\inter (B\setminus A) = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{setminus_partition} + Suppose $A\subseteq B$. + $A\union (B\setminus A) = B$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{subseteq_union_setminus} + $A\subseteq B\union (A\setminus B)$. +\end{proposition} + +\begin{proposition}\label{double_complement} + Suppose $A\subseteq B\subseteq C$. + Then $B\setminus (C\setminus A) = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{double_complement_union} + Then $(A\union B)\setminus (B\setminus A) = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{setminus_eq_inter_complement} + Suppose $A, B\subseteq C$. + Then $A\setminus B = A\inter (C\setminus B)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\subsection{Tuples} + +As with unordered pairs, +orderd pairs are a primitive construct and +$n$-tuples desugar to iterated applications of the +primitive operator $({-},{-})$. +For example $(a, b, c, d)$ equals $(a, (b, (c, d)))$ by definition. +While ordered pairs could be encoded set-theoretically, %(choosing Kuratowski's, Hausdorff's, or Wiener's encoding), +we simply postulate the defining property to prevent misguiding +proof automation. + +\begin{axiom}\label{pair_eq_iff} + $(a, b) = (a', b')$ iff $a = a'\land b = b'$. +\end{axiom} + +\begin{axiom}\label{pair_neq_emptyset} + $(a, b) \neq \emptyset$. +\end{axiom} + +\begin{axiom}\label{pair_neq_fst} + $(a, b) \neq a$. +\end{axiom} + +\begin{axiom}\label{pair_neq_snd} + $(a, b) \neq b$. +\end{axiom} + +Repeated application of the defining property of pairs yields the defining property of +all tuples. + +\begin{proposition}\label{triple_eq_iff} + $(a, b, c) = (a', b', c')$ iff $a = a' \land b = b'\land c = c'$. +\end{proposition} + +There are primitive projections $\fst{}$ and $\snd{}$ that satisfy the following axioms. + +\begin{axiom}\label{fst_eq} + $\fst{(a, b)} = a$. +\end{axiom} + +\begin{axiom}\label{snd_eq} + $\snd{(a, b)} = b$. +\end{axiom} + +\begin{proposition}\label{pair_eq_pair_of_proj} + $(a, b) = (\fst{(a,b)},\snd{(a,b)})$. +\end{proposition} + + +\begin{definition}\label{times} + $A\times B = \{ (a,b) \mid a\in A, b\in B \}$. +\end{definition} + +\begin{proposition}\label{times_tuple_elim} + Suppose $(x, y)\in X\times Y$. Then $x\in X$ and $y\in Y$. +\end{proposition} +\begin{proof} + Take $x', y'$ such that $x'\in X\land y'\in Y \land (x, y) = (x', y')$ + by \cref{times}. + Then $x = x'$ and $y = y'$ by \cref{pair_eq_iff}. +\end{proof} + +\begin{proposition}\label{times_tuple_intro} + Suppose $x\in X$ and $y\in Y$. Then $(x, y)\in X\times Y$. +\end{proposition} + +\begin{proposition}\label{times_empty_left} + $\emptyset\times Y = \emptyset$. +\end{proposition} + +\begin{proposition}\label{times_empty_right} + $X\times \emptyset = \emptyset$. +\end{proposition} + +\begin{proposition}\label{times_empty_iff} + $X\times Y$ is empty iff $X$ is empty or $Y$ is empty. +\end{proposition} +\begin{proof} + Follows by \cref{inhabited,times}. +\end{proof} + +\begin{proposition}\label{fst_type} + Suppose $c\in A\times B$. Then $\fst{c}\in A$. +\end{proposition} +\begin{proof} + Take $a, b$ such that $c = (a, b)$ and $a\in A$ + by \cref{times}. + $a = \fst{c}$ + by \cref{fst_eq}. +\end{proof} + +\begin{proposition}\label{snd_type} + Suppose $c\in A\times B$. Then $\snd{c}\in B$. +\end{proposition} +\begin{proof} + Take $a, b$ such that $c = (a, b)$ and $b\in B$ + by \cref{times}. + $b = \snd{c}$ + by \cref{snd_eq}. +\end{proof} + +\begin{proposition}\label{times_elem_is_tuple} + Suppose $p\in X\times Y$. Then there exist $x, y$ + such that $x\in X$ and $y\in Y$ and $p = (x, y)$. +\end{proposition} + + +\begin{proposition}\label{times_proj_elim} + Suppose $p\in X\times Y$. Then $\fst{p}\in X$ and $\snd{p}\in Y$. +\end{proposition} diff --git a/library/set/bipartition.tex b/library/set/bipartition.tex new file mode 100644 index 0000000..e6a76dc --- /dev/null +++ b/library/set/bipartition.tex @@ -0,0 +1,72 @@ +% The theory of splitting sets into two (inhabited, disjoint) partitions. + +% See also "bisections" here: https://isarmathlib.org/Partitions_ZF.html + +\import{set.tex} +\import{set/cons.tex} +\import{set/powerset.tex} + +\subsection{Bipartitions} + +\begin{abbreviation}\label{bipartitions} + $C$ is partitioned by $A$ and $B$ iff $A,B\neq\emptyset$ and $A$ is disjoint from $B$ and $A\union B = C$. +\end{abbreviation} + +\begin{definition}\label{bipartitions_of_a_set} + $\bipartitions{X} = \{ p\in\pow{X}\times\pow{X}\mid \text{$X$ is partitioned by $\fst{p}$ and $\snd{p}$}\}$. +\end{definition} + +\begin{abbreviation}\label{is_a_bipartition_of} + $P$ is a bipartition of $X$ iff $P\in\bipartitions{X}$. +\end{abbreviation} + +\begin{proposition}\label{bipartition_intro} + Suppose $C$ is partitioned by $A$ and $B$. + Then $(A, B)$ is a bipartition of $C$. +\end{proposition} +\begin{proof} + $(A,B)\in\pow{C}\times\pow{C}$. + $C$ is partitioned by $\fst{(A,B)}$ and $\snd{(A,B)}$. + Thus $(A, B)$ is a bipartition of $C$ by \cref{bipartitions_of_a_set}. +\end{proof} + +\begin{proposition}\label{bipartition_elim} + Suppose $(A, B)$ is a bipartition of $C$. + Then $C$ is partitioned by $A$ and $B$. +\end{proposition} +\begin{proof} + $\fst{(A, B)} = A$. + $\snd{(A, B)} = B$. +\end{proof} + +\begin{proposition}\label{bipartitions_emptyset} + $\bipartitions{\emptyset}$ is empty. +\end{proposition} + +\begin{proposition}\label{union_eq_cons_implies_union_remove_eq} + Suppose $d\notin C$. + Suppose $A\union B = \cons{d}{C}$. + Suppose $A, B\neq \{d\}$. + Then $\remove{d}{A}\union \remove{d}{B} = C$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{bipartitions_cons} + Suppose $d\notin C$. + Suppose $\cons{d}{C}$ is partitioned by $A$ and $B$. + Suppose $A, B\neq \{d\}$. + Then $C$ is partitioned by $\remove{d}{A}$ and $\remove{d}{B}$. +\end{proposition} +\begin{proof} + $\remove{d}{A},\remove{d}{B}\neq\emptyset$. + $\remove{d}{A}\union \remove{d}{B} = C$ by \cref{union_eq_cons_implies_union_remove_eq}. +\end{proof} + +% TODO +%\begin{proposition}\label{singleton_bipartition} +% Suppose $b\notin A$. +% Suppose $A$ and $\{b\}$ bipartition $\cons{b}{C}$. +% Then $A = C$. +%\end{proposition} diff --git a/library/set/cantor.tex b/library/set/cantor.tex new file mode 100644 index 0000000..f7c4b2b --- /dev/null +++ b/library/set/cantor.tex @@ -0,0 +1,18 @@ +\import{set/powerset.tex} +\import{function.tex} + +\subsection{Cantor's theorem} + + +\begin{theorem}[Cantor]\label{cantor} + There exists no surjection from $A$ to $\pow{A}$. +\end{theorem} +\begin{proof} + Suppose not. + Consider a surjection $f$ from $A$ to $\pow{A}$. + Let $B = \{a \in A \mid a\notin f(a)\}$. + Then $B\in\pow{A}$. + There exists $a'\in A$ such that $f(a') = B$ by \hyperref[surj]{the definition of surjectivity}. + Now $a' \in B$ iff $a' \notin f(a') = B$. + Contradiction. +\end{proof} diff --git a/library/set/cons.tex b/library/set/cons.tex new file mode 100644 index 0000000..e03ba4f --- /dev/null +++ b/library/set/cons.tex @@ -0,0 +1,112 @@ +\import{set.tex} + +\subsection{Additional results about cons} + +\begin{proposition}\label{cons_subseteq_intro} + Suppose $x\in X$. + Suppose $Y\subseteq X$. + Then $\cons{x}{Y}\subseteq X$. +\end{proposition} + +\begin{proposition}\label{cons_subseteq_elim} + Suppose $\cons{x}{Y}\subseteq X$. + Then $x\in X$ and $Y\subseteq X$. +\end{proposition} + +\begin{proposition}\label{cons_subseteq_iff} + $\cons{x}{Y}\subseteq X$ iff $x\in X$ and $Y\subseteq X$. +\end{proposition} + +\begin{proposition}\label{subseteq_cons_right} + If $C\subseteq B$, then $C\subseteq \cons{a}{B}$. +\end{proposition} + +\begin{corollary}\label{subseteq_cons_self} + $X\subseteq \cons{y}{X}$. +\end{corollary} + +\begin{abbreviation}\label{remove_point} + $\remove{a}{B} = B\setminus\{a\}$. +\end{abbreviation} + +\begin{proposition}\label{subseteq_cons_intro_left} + Suppose $a\in C \land \remove{a}{C} \subseteq B$. + Then $C\subseteq \cons{a}{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{setminus_cons,setminus_eq_emptyset_iff_subseteq}. +\end{proof} + +\begin{proposition}\label{subseteq_cons_intro_right} + Suppose $C \subseteq B$. + Then $C\subseteq \cons{a}{B}$. +\end{proposition} + +\begin{proposition}\label{subseteq_cons_elim} + Suppose $C\subseteq \cons{a}{B}$. + Then $C\subseteq B \lor (a\in C \land \remove{a}{C} \subseteq B)$. +\end{proposition} +\begin{proof} + Follows by \cref{setminus_cons,subseteq,cons_iff,setminus_eq_emptyset_iff_subseteq}. +\end{proof} + +\begin{proposition}\label{subseteq_cons_iff} + $C\subseteq \cons{a}{B}$ iff $C\subseteq B \lor (a\in C \land \remove{a}{C}\subseteq B)$. +\end{proposition} + + +\begin{proposition}\label{remove_point_eq_setminus_singleton} + $\remove{a}{B} = B\setminus\{a\}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + + +\begin{proposition}\label{union_eq_cons} + $\{a\}\union B = \cons{a}{B}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{cons_comm} + $\cons{a}{\cons{b}{C}} = \cons{b}{\cons{a}{C}}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{cons_absorb} + Suppose $a\in A$. + Then $\cons{a}{A} = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{cons_remove} + Suppose $a\in A$. + Then $\cons{a}{A\setminus\{a\}} = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{cons_idempotent} + Then $\cons{a}{\cons{a}{B}} = \cons{a}{B}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{inters_cons} + Suppose $B$ is inhabited. + Then $\inters{\cons{a}{B}} = a\inter\inters{B}$. +\end{proposition} +\begin{proof} + $\cons{a}{B}$ is inhabited. + Thus for all $c$ we have $c\in\inters{\cons{a}{B}}$ iff $c\in a\inter \inters{B}$ + by \cref{inters_iff_forall,cons_iff,inter}. + Follows by \hyperref[setext]{extensionality}. +\end{proof} diff --git a/library/set/equinumerosity.tex b/library/set/equinumerosity.tex new file mode 100644 index 0000000..a846b78 --- /dev/null +++ b/library/set/equinumerosity.tex @@ -0,0 +1,68 @@ +\import{set/powerset.tex} +\import{set/fixpoint.tex} +\import{function.tex} + + +\begin{definition}\label{equinum} + $A$ is equinumerous with $B$ iff there exists a bijection from $A$ to $B$. +\end{definition} + +\begin{abbreviation}\label{approx} + $A\approx B$ iff $A$ is equinumerous with $B$. +\end{abbreviation} + +\begin{proposition}\label{equinum_refl} + $A\approx A$. +\end{proposition} +\begin{proof} + $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_is_bijection}. + Follows by \cref{equinum}. +\end{proof} + +\begin{proposition}\label{equinum_sym} + Suppose $A\approx B$. Then $B\approx A$. +\end{proposition} +\begin{proof} + Take a bijection $f$ from $A$ to $B$ by \cref{equinum}. + Then $\converse{f}$ is a bijection from $B$ to $A$ by \cref{bijection_converse_is_bijection}. + Follows by \cref{equinum}. +\end{proof} + +\begin{proposition}\label{equinum_tran} + Suppose $A\approx B\approx C$. Then $A\approx C$. +\end{proposition} +\begin{proof} + Take a bijection $f$ from $A$ to $B$ by \cref{equinum}. + Take a bijection $g$ from $B$ to $C$ by \cref{equinum}. + Then $g\circ f$ is a bijection from $A$ to $C$ by \cref{bijection_circ}. + Follows by \cref{equinum}. +\end{proof} + + + +\begin{theorem}[Cantor--Schröder--Bernstein]\label{cantorschroederbernstein} + Let $f$ be an injective function from $A$ to $B$. + Let $g$ be an injective function from $B$ to $A$. + Then $A\approx B$. +\end{theorem} +\begin{proof} + Let $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$ for $X\in\pow{A}$. + %By construction: $h$ is a relation. + %By construction: $h$ is right-unique. + %By construction: $\dom{h} = \pow{A}$. + For all $X\in\pow{A}$ we have $h(X)\in\pow{A}$ by \cref{setminus_subseteq,pow_iff}. + Thus $h$ is a function from $\pow{A}$ to $\pow{A}$. + + $h$ is \subseteq-preserving by \cref{subseteqpreserving,img_subseteq,subseteq_implies_setminus_supseteq}. % apply each each lemma twice (alternating). + + Take a fixpoint $X$ of $h$ by \cref{knastertarski}. + Now $X = A\setminus \img{g}{B\setminus\img{f}{X}}$ by \cref{fixpoint}. + + $\img{g}{B\setminus\img{f}{X}}\subseteq A$. + + Thus $\img{g}{B\setminus\img{f}{X}} = A\setminus X$ by \cref{double_relative_complement}. + + Let $h' = \restrl{h}{X}$. + + Omitted. % TODO +\end{proof} diff --git a/library/set/filter.tex b/library/set/filter.tex new file mode 100644 index 0000000..2797d86 --- /dev/null +++ b/library/set/filter.tex @@ -0,0 +1,97 @@ +\import{set.tex} +\import{set/powerset.tex} + +\section{Filters} + +\begin{abbreviation}\label{upwardclosed} + $F$ is upward-closed in $S$ iff + for all $A, B$ such that $A\subseteq B\subseteq S$ and $A\in F$ we have $B\in F$. +\end{abbreviation} + +\begin{definition}\label{filter} + $F$ is a filter on $S$ iff + $F$ is a family of subsets of $S$ + and $S$ is inhabited + and $S\in F$ + and $\emptyset\notin F$ + and $F$ is closed under binary intersections + and $F$ is upward-closed in $S$. +\end{definition} + +\begin{definition}\label{principalfilter} + $\principalfilter{S}{A} = \{X\in\pow{S}\mid A\subseteq X\}$. +\end{definition} + +%\begin{proposition}\label{principalfilter_domain_inhabited} +% Suppose $F$ is a filter on $S$. +% Then $S$ is inhabited. +%\end{proposition} + +\begin{proposition}\label{principalfilter_is_filter} + Suppose $A\subseteq S$. + Suppose $A$ is inhabited. + Then $\principalfilter{S}{A}$ is a filter on $S$. +\end{proposition} +\begin{proof} + $S$ is inhabited. % since $A$ is inhabited and $A\subseteq S$. + $\principalfilter{S}{A}$ is a family of subsets of $S$. + $S\in \principalfilter{S}{A}$. + $\emptyset\notin \principalfilter{S}{A}$. + $\principalfilter{S}{A}$ is closed under binary intersections. + $\principalfilter{S}{A}$ is upward-closed in $S$. + Follows by \cref{filter}. +\end{proof} + +\begin{proposition}\label{principalfilter_elem_generator} + Suppose $A\subseteq S$. + $A\in\principalfilter{S}{A}$. +\end{proposition} +\begin{proof} + $A\in\pow{S}$. +\end{proof} + +\begin{proposition}\label{principalfilter_notelem_implies_notsupseteq} + Let $X\in\pow{S}$. + Suppose $X\notin\principalfilter{S}{A}$. + Then $A\not\subseteq X$. +\end{proposition} +\begin{proof} +\end{proof} + +\begin{definition}\label{maximalfilter} + $F$ is a maximal filter on $S$ iff + $F$ is a filter on $S$ and there exists no filter $F'$ on $S$ such that $F\subset F'$. +\end{definition} + +\begin{proposition}\label{principalfilter_singleton_is_filter} + Suppose $a\in S$. + Then $\principalfilter{S}{\{a\}}$ is a filter on $S$. +\end{proposition} +\begin{proof} + $\{a\}\subseteq S$. + $\{a\}$ is inhabited. + Follows by \cref{principalfilter_is_filter}. +\end{proof} + +\begin{proposition}\label{principalfilter_singleton_is_maximal_filter} + Suppose $a\in S$. + Then $\principalfilter{S}{\{a\}}$ is a maximal filter on $S$. +\end{proposition} +\begin{proof} + $\{a\}\subseteq S$. + $\{a\}$ is inhabited. + Thus $\principalfilter{S}{\{a\}}$ is a filter on $S$ by \cref{principalfilter_is_filter}. + It suffices to show that there exists no filter $F'$ on $S$ such that $\principalfilter{S}{\{a\}}\subset F'$. + Suppose not. + Take a filter $F'$ on $S$ such that $\principalfilter{S}{\{a\}}\subset F'$. + Take $X\in F'$ such that $X\notin \principalfilter{S}{\{a\}}$. + $X\in\pow{S}$. + Thus $\{a\}\not\subseteq X$ by \cref{principalfilter_notelem_implies_notsupseteq}. + Thus $a\notin X$. + $\{a\}\in F'$ + % TODO clean + by \cref{principalfilter,elem_subseteq,union_intro_left,subset,union_absorb_subseteq_left,subseteq_refl,powerset_intro}. + Thus $\emptyset = X\inter \{a\}$. + Hence $\emptyset\in F'$ by \cref{filter}. + Follows by \hyperref[filter]{contradiction to the definition of a filter}. +\end{proof} diff --git a/library/set/fixpoint.tex b/library/set/fixpoint.tex new file mode 100644 index 0000000..700295b --- /dev/null +++ b/library/set/fixpoint.tex @@ -0,0 +1,48 @@ +\import{set/powerset.tex} +\import{function.tex} + +\subsection{Fixpoints} + +% NOTE: we need to explicitly require that a is an element of the domain, +% otherwise the emptyset becomes a fixpoint when it's not in the domain. +\begin{definition}\label{fixpoint} + $a$ is a fixpoint of $f$ iff $a\in\dom{f}$ and $f(a) = a$. +\end{definition} + +\begin{definition}\label{subseteqpreserving} + $f$ is \subseteq-preserving iff + for all $A, B\in\dom{f}$ such that $A\subseteq B$ we have $f(A)\subseteq f(B)$. +\end{definition} + +\begin{theorem}[Knaster--Tarski]\label{knastertarski} + Let $f$ be a \subseteq-preserving function from $\pow{A}$ to $\pow{A}$. + Then there exists a fixpoint of $f$. +\end{theorem} +\begin{proof} + $\dom{f} = \pow{A}$. + Let $P = \{a\in\pow{A}\mid a\subseteq f(a)\}$. + $P\subseteq\pow{A}$. + Thus $\unions{P}\in\pow{A}$. + Hence $f(\unions{P})\in\pow{A}$ by \cref{funs_type_apply}. + + Show $\unions{P}\subseteq f(\unions{P})$. + \begin{subproof} + It suffices to show that every element of $\unions{P}$ is an element of $f(\unions{P})$. + % + Fix $u\in\unions{P}$. + % + Take $p\in P$ such that $u\in p$. + Then $u\in f(p)$. + $p\subseteq\unions{P}$. + $f(p)\subseteq f(\unions{P})$ by \cref{subseteqpreserving}. + Thus $u\in f(\unions{P})$. + \end{subproof} + + Now $f(\unions{P})\subseteq f(f(\unions{P}))$ by \cref{subseteqpreserving}. + Thus $f(\unions{P})\in P$ by definition. + + Hence $f(\unions{P})\subseteq \unions{P}$. + + Thus $f(\unions{P}) = \unions{P}$ by \cref{subseteq_antisymmetric}. + Follows by \cref{fixpoint}. +\end{proof} diff --git a/library/set/partition.tex b/library/set/partition.tex new file mode 100644 index 0000000..ed74bf7 --- /dev/null +++ b/library/set/partition.tex @@ -0,0 +1,50 @@ +\import{set.tex} + +\subsection{Partitions} + +\begin{definition}\label{partition} + $P$ is a partition iff + $\emptyset\notin P$ and + for all $B, C\in P$ such that $B\neq C$ we have $B$ is disjoint from $C$. +\end{definition} + +\begin{abbreviation}\label{partition_of} + $P$ is a partition of $A$ iff + $P$ is a partition and + $\unions{P} = A$. +\end{abbreviation} + +\begin{proposition}\label{partition_emptyset} + $\emptyset$ is a partition of $\emptyset$. +\end{proposition} + +\begin{definition}\label{partition_refinement} + $P'$ is a refinement of $P$ iff + for every $A'\in P'$ there exists + $A\in P$ such that $A'\subseteq A$. +\end{definition} + +\begin{abbreviation}\label{partition_refines} + $P'\refines P$ iff + $P'$ is a refinement of $P$. +\end{abbreviation} + +\begin{proposition}\label{partition_refinement_transitive} + Suppose $P''\refines P'\refines P$. + Then $P''\refines P$. +\end{proposition} +\begin{proof} + It suffices to show that for all $A''\in P''$ there exists $A\in P$ such that $A''\subseteq A$. + Fix $A''\in P''$. + Take $A'\in P'$ such that $A''\subseteq A'$ + by \cref{partition_refinement}. + Take $A\in P$ such that $A'\subseteq A$. + Then $A''\subseteq A$. + Follows by definition. %i.e. A will do for the current existential goal. +\end{proof} + +%\begin{definition}\label{set_of_representatives} +% $X$ is a set of representatives for $P$ iff +% for all $A\in P$ there exists $a\in A$ such that +% $X\inter A = \{a\}$. +%\end{definition} diff --git a/library/set/powerset.tex b/library/set/powerset.tex new file mode 100644 index 0000000..80da4cb --- /dev/null +++ b/library/set/powerset.tex @@ -0,0 +1,107 @@ +\import{set.tex} + +\subsection{Powerset} + +\begin{abbreviation}\label{powerset_of} + The powerset of $X$ denotes $\pow{X}$. +\end{abbreviation} + +\begin{axiom}% +\label{pow_iff} + $B\in\pow{A}$ iff $B\subseteq A$. +\end{axiom} + +\begin{proposition}\label{powerset_intro} + Suppose $A\subseteq B$. + Then $A\in\pow{B}$. +\end{proposition} + +\begin{proposition}\label{powerset_elim} + Let $A\in\pow{B}$. + Then $A\subseteq B$. +\end{proposition} + +\begin{proposition}\label{powerset_bottom} + $\emptyset\in\pow{A}$. +\end{proposition} + +\begin{proposition}\label{powerset_top} + $A\in\pow{A}$. +\end{proposition} + +\begin{proposition}\label{unions_subseteq_of_powerset_is_subseteq} + Let $A$ be a set. + Let $B$ be a subset of $\pow{A}$. + Then $\unions{B}\subseteq A$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,powerset_elim,unions_iff}. +\end{proof} + +\begin{corollary}\label{powerset_closed_unions} + Let $A$ be a set. + Let $B$ be a subset of $\pow{A}$. + Then $\unions{B}\in\pow{A}$. +\end{corollary} +\begin{proof} + Follows by \cref{pow_iff,unions_subseteq_of_powerset_is_subseteq}. +\end{proof} + +\begin{proposition}\label{unions_powerset} + $\unions{\pow{A}} = A$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{inters_powerset} + $\inters{\pow{A}} = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_powersets_subseteq} + $\pow{A}\union\pow{B} \subseteq \pow{A\union B}$. +\end{proposition} +\begin{proof} + $\pow{A}\subseteq \pow{A}\union\pow{B}$ by \cref{union_upper_left}. + $\pow{B}\subseteq \pow{A}\union\pow{B}$ by \cref{union_upper_right}. + Follows by \cref{subseteq,pow_iff,powerset_elim,union_iff,subset_transitive}. +\end{proof} + +\begin{proposition}\label{powerset_emptyset} + $\pow{\emptyset} = \{\emptyset\}$. +\end{proposition} + +% LATER +%\begin{proposition}\label{powerset_cons} +% Then $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$. +%\end{proposition} + +\begin{proposition}\label{powerset_union_subseteq} + $\pow{A}\union\pow{B}\subseteq \pow{A\union B}$. +\end{proposition} + +\begin{proposition}\label{subseteq_pow_unions} + $A\subseteq\pow{\unions{A}}$. +\end{proposition} +\begin{proof} + Follows by \cref{subseteq,pow_iff,unions_intro}. +\end{proof} + +\begin{proposition}\label{unions_pow} + $\unions{\pow{A}} = A$. +\end{proposition} + + +\begin{proposition}\label{unions_elem_pow_iff} + $\unions{A}\in\pow{B}$ iff $A\in\pow{\pow{B}}$. +\end{proposition} + +\begin{proposition}\label{pow_inter} + $\pow{A\inter B} = \pow{A}\inter\pow{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{setext,inter,pow_iff,subseteq_inter_iff}. +\end{proof} diff --git a/library/set/product.tex b/library/set/product.tex new file mode 100644 index 0000000..bc7d314 --- /dev/null +++ b/library/set/product.tex @@ -0,0 +1,118 @@ +\import{set.tex} + +\begin{proposition}\label{times_subseteq_left} + Suppose $A\subseteq C$. Then $A\times B\subseteq C\times B$. +\end{proposition} +\begin{proof} + It suffices to show that for all $w\in A\times B$ we have $w\in C\times B$. +\end{proof} + +\begin{proposition}\label{times_subseteq_right} + Suppose $B\subseteq D$. Then $A\times B\subseteq A\times D$. +\end{proposition} +\begin{proof} + It suffices to show that for all $w\in A\times B$ we have $w\in A\times D$. +\end{proof} + +\begin{proposition}\label{inter_times_intro} + Suppose $w\in(A\inter B)\times (C\inter D)$. + Then $w\in(A\times C)\inter (B\times D)$. +\end{proposition} +\begin{proof} + Take $a,c$ such that $w = (a, c)$ + by \cref{times_elem_is_tuple}. + Then $a\in A, B$ and $c\in C,D$ + by \cref{times_tuple_elim,inter}. + Thus $w\in (A\times C), (B\times D)$. +\end{proof} + +\begin{proposition}\label{inter_times_elim} + Suppose $w\in(A\times C)\inter (B\times D)$. + Then $w\in(A\inter B)\times (C\inter D)$. +\end{proposition} +\begin{proof} + $w\in A\times C$. + Take $a, c$ such that $w = (a, c)$. + $a\in A, B$ by \cref{inter,times_tuple_elim}. + $c\in C, D$ by \cref{inter,times_tuple_elim}. + Thus $(a,c) \in (A\inter B)\times (C\inter D)$ by \cref{times,inter_intro}. +\end{proof} + +\begin{proposition}\label{inter_times} + $(A\inter B)\times (C\inter D) = (A\times C)\inter (B\times D)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{inter_times_right} + $(X\inter Y)\times Z = (X\times Z)\inter (Y\times Z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{inter_times_left} + $X\times (Y\inter Z) = (X\times Y)\inter (X\times Z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_times_intro} + Suppose $w\in(A\union B)\times (C\union D)$. + Then $w\in(A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$. +\end{proposition} +\begin{proof} + Take $a,c$ such that $w = (a, c)$. + $a\in A$ or $a\in B$ by \cref{union_iff,times_tuple_elim}. + $c\in C$ or $c\in D$ by \cref{union_iff,times_tuple_elim}. + Thus $(a, c)\in (A\times C)$ or $(a, c)\in (B\times D)$ or $(a, c)\in (A\times D)$ or $(a, c)\in (B\times C)$. + Thus $(a, c)\in (A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$. +\end{proof} + +\begin{proposition}\label{union_times_elim} + Suppose $w\in(A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$. + Then $w\in(A\union B)\times (C\union D)$. +\end{proposition} +\begin{proof} + \begin{byCase} + \caseOf{$w\in(A\times C)$.} + Take $a, c$ such that $w = (a, c) \land a\in A\land c\in C$ by \cref{times}. + Then $a\in A\union B$ and $c\in C\union D$. + Follows by \cref{times_tuple_intro}. + \caseOf{$w\in(B\times D)$.} + Take $b, d$ such that $w = (b, d) \land b\in B\land d\in D$ by \cref{times}. + Then $b\in A\union B$ and $d\in C\union D$. + Follows by \cref{times_tuple_intro}. + \caseOf{$w\in(A\times D)$.} + Take $a, d$ such that $w = (a, d) \land a\in A\land d\in D$ by \cref{times}. + Then $a\in A\union B$ and $d\in C\union D$. + Follows by \cref{times_tuple_intro}. + \caseOf{$w\in(B\times C)$.} + Take $b, c$ such that $w = (b, c) \land b\in B\land c\in C$ by \cref{times}. + Then $b\in A\union B$ and $c\in C\union D$. + Follows by \cref{times_tuple_intro}. + \end{byCase} +\end{proof} + +\begin{proposition}\label{union_times} + $(A\union B)\times (C\union D) = (A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_times_left} + $(X\union Y)\times Z = (X\times Z)\union (Y\times Z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{union_times_right} + $X\times (Y\union Z) = (X\times Y)\union (X\times Z)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} diff --git a/library/set/regularity.tex b/library/set/regularity.tex new file mode 100644 index 0000000..794d34f --- /dev/null +++ b/library/set/regularity.tex @@ -0,0 +1,70 @@ +\import{set.tex} + +\section{Regularity} + +\begin{abbreviation}\label{elemminimal} + $a$ is an \in-minimal element of $A$ iff + $a\in A$ and $a\notmeets A$. +\end{abbreviation} + +% We need to first state regularity in this slightly weirder form, +% so that we can do \in-induction. +\begin{lemma}% +\label{regularity_aux} + For all $a, A$ such that $a\in A$ + there exists $b\in A$ such that + $b\notmeets A$. +\end{lemma} +\begin{proof}[Proof by \in-induction on $a$] + \begin{byCase} + \caseOf{$a\notmeets b$.} + Straightforward. + \caseOf{$a\meets b$.} + Take $a'$ such that $a'\in a, b$. + Straightforward. % we apply the induction hypothesis to a' + \end{byCase} +\end{proof} + +\begin{proposition}[Regularity]% +\label{regularity} + Let $A$ be an inhabited set. + Then there exists a \in-minimal element of $A$. +\end{proposition} +\begin{proof} + Follows by \cref{regularity_aux,inhabited}. +\end{proof} + + +% Isabelle/ZF-style foundation for case analysis +\begin{theorem}[Foundation]\label{foundation} + Let $A$ be a set. + Then $A = \emptyset$ or there exists $a\in A$ + such that for all $x\in a$ we have $x\notin A$. +\end{theorem} +\begin{proof} + \begin{byCase} + \caseOf{$A = \emptyset$.} + Straightforward. + \caseOf{$A$ is inhabited.} + Take $a$ such that $a$ is a \in-minimal element of $A$. + Then for all $x\in a$ we have $x\notin A$. + \end{byCase} +\end{proof}. + +\begin{proposition}\label{in_irrefl} + For all sets $A$ we have $A\not\in A$. +\end{proposition} +\begin{proof}[Proof by \in-induction] + Straightforward. +\end{proof} + +\begin{proposition}\label{in_implies_neq} + If $a\in A$, then $a\neq A$. +\end{proposition} + +\begin{proposition}\label{in_asymmetric} + For all sets $a, b$ such that $a\in b$ we have $b\notin a$. +\end{proposition} +\begin{proof}[Proof by \in-induction on $a$] + Straightforward. +\end{proof} diff --git a/library/set/suc.tex b/library/set/suc.tex new file mode 100644 index 0000000..3776045 --- /dev/null +++ b/library/set/suc.tex @@ -0,0 +1,70 @@ +\import{set/cons.tex} +\import{set/regularity.tex} + +\subsection{Successor} + +\begin{definition}\label{suc} + $\suc{x} = \cons{x}{x}$. +\end{definition} + +\begin{proposition}\label{suc_intro_self} + $x\in\suc{x}$. +\end{proposition} + +\begin{proposition}\label{suc_intro_in} + Suppose $x\in y$. Then $x\in\suc{y}$. +\end{proposition} + +\begin{proposition}\label{suc_elim} + Suppose $x\in\suc{y}$. + Then $x = y$ or $x\in y$. +\end{proposition} + +\begin{proposition}\label{suc_iff} + $x\in\suc{y}$ iff $x = y$ or $x\in y$. +\end{proposition} + +\begin{proposition}\label{suc_neq_emptyset} + $\suc{x}\neq \emptyset$. +\end{proposition} + +\begin{proposition}\label{suc_subseteq_implies_in} + Suppose $\suc{x}\subseteq y$. Then $x\in y$. +\end{proposition} + +\begin{proposition}\label{suc_neq_self} + $\suc{x}\neq x$. +\end{proposition} + +\begin{proposition}\label{suc_injective} + Suppose $\suc{x} = \suc{y}$. Then $x = y$. +\end{proposition} +\begin{proof} + Suppose not. + $\suc{x}\subseteq \suc{y}$. Hence $x\in\suc{y}$. + Then $x\in y$. + $\suc{y}\subseteq \suc{x}$. Hence $y\in\suc{x}$. + Then $y\in x$. + Contradiction. +\end{proof} + +\begin{proposition}\label{subseteq_self_suc_intro} + $x\subseteq\suc{x}$. +\end{proposition} + +\begin{proposition}\label{suc_subseteq_intro} + Suppose $x\in y$ and $x\subseteq y$. + Then $\suc{x}\subseteq y$. +\end{proposition} + +\begin{proposition}\label{suc_subseteq_elim} + Suppose $\suc{x}\subseteq y$. + Then $x\in y$ and $x\subseteq y$. +\end{proposition} + +\begin{proposition}\label{suc_next_subset} + There exists no $z$ such that $x\subset z\subset \suc{x}$. +\end{proposition} +\begin{proof} + Follows by \cref{suc,subset,subseteq,subset_witness,suc_elim}. +\end{proof} diff --git a/library/set/symdiff.tex b/library/set/symdiff.tex new file mode 100644 index 0000000..61f7448 --- /dev/null +++ b/library/set/symdiff.tex @@ -0,0 +1,45 @@ +\subsection{Symmetric difference} + +\import{set.tex} + +\begin{definition}\label{symdiff} + $x\symdiff y = (x\setminus y)\union (y\setminus x)$. +\end{definition} + +\begin{proposition}% +\label{symdiff_as_setdiff} + $x\symdiff y = (x\union y)\setminus (y\inter x)$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{symdiff_implies_xor_in} + If $z\in x\symdiff y$, then either $z\in x$ or $z\in y$. +\end{proposition} + +\begin{proposition}% +\label{xor_in_implies_symdiff} + If either $z\in x$ or $z\in y$, then $z\in x\symdiff y$. +\end{proposition} +\begin{proof} + If $z\in x$ and $z\not\in y$, then $z\in x\setminus y$. + If $z\not\in x$ and $z\in y$, then $z\in y\setminus x$. +\end{proof} + +\begin{proposition}% +\label{symdiff_assoc} + $x\symdiff (y\symdiff z) = (x\symdiff y)\symdiff z$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}% +\label{symdiff_comm} + $x\symdiff y = y\symdiff x$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} diff --git a/library/subfinite.tex b/library/subfinite.tex new file mode 100644 index 0000000..bc1a781 --- /dev/null +++ b/library/subfinite.tex @@ -0,0 +1,12 @@ +\import{function.tex} +\import{nat.tex} + +\begin{definition}\label{subfinite} + $X$ is subfinite iff + there exists a natural number $k$ such that + there exists an injective function $f$ from $k$ to $X$. +\end{definition} + +\begin{proposition}\label{emptyset_subfinite} + $\emptyset$ is subfinite. +\end{proposition} diff --git a/library/topology/basis.tex b/library/topology/basis.tex new file mode 100644 index 0000000..dda187c --- /dev/null +++ b/library/topology/basis.tex @@ -0,0 +1,45 @@ +\import{topology/topological-space.tex} + +\subsection{Topological basis} + +\begin{abbreviation}\label{covers} + $C$ covers $X$ iff + for all $x\in X$ there exists $U\in C$ such that $x\in U$. +\end{abbreviation} + +\begin{proposition}\label{covers_unions_intro} + Suppose $C$ covers $X$. + Then $X\subseteq\unions{C}$. +\end{proposition} + +\begin{proposition}\label{covers_unions_elim} + Suppose $X\subseteq\unions{C}$. + Then $C$ covers $X$. +\end{proposition} + +% Also called "prebase", "subbasis", or "subbase". We prefer "pre-" or "quasi-" +% for consistency when handling generalizations, even if "subbasis" is more common. +\begin{abbreviation}\label{topological_prebasis} + $B$ is a topological prebasis for $X$ iff $\unions{B} = X$. +\end{abbreviation} + +\begin{proposition}\label{topological_prebasis_iff_covering_family} + $B$ is a topological prebasis for $X$ iff + $B$ is a family of subsets of $X$ and $B$ covers $X$. +\end{proposition} +\begin{proof} + If $B$ is a family of subsets of $X$ and $B$ covers $X$, + then $\unions{B} = X$ + by \cref{subseteq_antisymmetric,unions_family,covers_unions_intro}. + If $\unions{B} = X$, + then $B$ is a family of subsets of $X$ and $B$ covers $X$ + by \cref{covers_unions_intro,subseteq_refl,covers_unions_elim}. +\end{proof} + +% Also called "base of topology". +\begin{definition}\label{topological_basis} + $B$ is a topological basis for $X$ iff + $B$ is a topological prebasis for $X$ and + for all $U, V, x$ such that $U, V\in B$ and $x\in U,V$ + there exists $W\in B$ such that $x\in W\subseteq U, V$. +\end{definition} diff --git a/library/topology/disconnection.tex b/library/topology/disconnection.tex new file mode 100644 index 0000000..e3730f3 --- /dev/null +++ b/library/topology/disconnection.tex @@ -0,0 +1,44 @@ +\import{set.tex} +\import{set/bipartition.tex} +\import{topology/topological-space.tex} + +\subsection{Disconnections} + +\begin{definition}\label{disconnections} + $\disconnections{X} = \{ p\in\bipartitions{\carrier[X]} \mid \text{$\fst{p},\snd{p}\in\opens[X]$} \}$. +\end{definition} + +\begin{abbreviation}\label{is_a_disconnection} + $D$ is a disconnection of $X$ iff $D\in\disconnections{X}$. +\end{abbreviation} + +\begin{definition}\label{disconnected} + $X$ is disconnected iff there exist $U, V\in\opens[X]$ + such that $\carrier[X]$ is partitioned by $U$ and $V$. +\end{definition} + +\begin{proposition}\label{disconnection_from_disconnected} + Let $X$ be a topological space. + Suppose $X$ is disconnected. + Then there exists a disconnection of $X$. +\end{proposition} +\begin{proof} + Take $U, V\in\opens[X]$ such that $\carrier[X]$ is partitioned by $U$ and $V$ + by \cref{disconnected}. + Then $(U, V)$ is a bipartition of $\carrier[X]$. + Thus $(U, V)$ is a disconnection of $X$ by \cref{disconnections,times_proj_elim,times_tuple_intro}. +\end{proof} + +\begin{proposition}\label{disconnected_from_disconnection} + Let $X$ be a topological space. + Let $D$ be a disconnection of $X$. + Then $X$ is disconnected. +\end{proposition} +\begin{proof} + $\fst{D}, \snd{D}\in\opens[X]$. + $\carrier[X]$ is partitioned by $\fst{D}$ and $\snd{D}$. +\end{proof} + +\begin{abbreviation}\label{connected} + $X$ is connected iff $X$ is not disconnected. +\end{abbreviation} diff --git a/library/topology/preclosure.tex b/library/topology/preclosure.tex new file mode 100644 index 0000000..6c104be --- /dev/null +++ b/library/topology/preclosure.tex @@ -0,0 +1,18 @@ +\import{set.tex} + +\section{Preclosure spaces} + + +\begin{struct} + A preclosure space $X$ is a onesorted structure equipped with + \begin{enumerate} + \item $\cl$ + \end{enumerate} + such that + \begin{enumerate} + \item For all $Y\subseteq X$ we have $\cl(Y)\subseteq X$. + \item $\cl(\emptyset) = \emptyset$. + \item For all $A$ we have $A\subseteq \cl(A)$. + \item For all $A, B$ we have $\cl(A\union B) = \cl(A) \union \cl(B)$. + \end{enumerate} +\end{struct} diff --git a/library/topology/separation.tex b/library/topology/separation.tex new file mode 100644 index 0000000..f70cb50 --- /dev/null +++ b/library/topology/separation.tex @@ -0,0 +1,124 @@ +\import{topology/topological-space.tex} + + +% T0 separation +\begin{definition}\label{is_kolmogorov} + $X$ is Kolmogorov iff + for all $x,y\in\carrier[X]$ such that $x\neq y$ + there exist $U\in\opens[X]$ such that + $x\in U\not\ni y$ or $x\notin U\ni y$. +\end{definition} + +\begin{abbreviation}\label{kolmogorov_space} + $X$ is a Kolmogorov space iff $X$ is a topological space and + $X$ is Kolmogorov. +\end{abbreviation} + +\begin{abbreviation}\label{teezero} + $X$ is \teezero\ iff $X$ is Kolmogorov. +\end{abbreviation} + +\begin{abbreviation}\label{teezero_space} + $X$ is a \teezero-space iff $X$ is a Kolmogorov space. +\end{abbreviation} + +\begin{proposition}\label{kolmogorov_implies_kolmogorov_for_closeds} + Suppose $X$ is a Kolmogorov space. + Let $x,y\in\carrier[X]$. + Suppose $x\neq y$. + Then there exist $A\in\closeds{X}$ such that + $x\in A\not\ni y$ or $x\notin A\ni y$. +\end{proposition} +\begin{proof} + Take $U\in\opens[X]$ such that $x\in U\not\ni y$ or $x\notin U\ni y$ + by \cref{is_kolmogorov}. + Then $\carrier[X]\setminus U\in\closeds{X}$ by \cref{complement_of_open_elem_closeds}. + Now $x\in (\carrier[X]\setminus U)\not\ni y$ or $x\notin (\carrier[X]\setminus U)\ni y$ + by \cref{setminus}. +\end{proof} + +\begin{proposition}\label{kolmogorov_for_closeds_implies_kolmogorov} + Suppose for all $x,y\in\carrier[X]$ such that $x\neq y$ + there exist $U\in\closeds{X}$ such that + $x\in U\not\ni y$ or $x\notin U\ni y$. + Then $X$ is Kolmogorov. +\end{proposition} +\begin{proof} + Follows by \cref{closeds,is_closed_in,is_kolmogorov,setminus}. +\end{proof} + +\begin{proposition}\label{kolmogorov_iff_kolmogorov_for_closeds} + Let $X$ be a topological space. + $X$ is Kolmogorov iff + for all $x,y\in\carrier[X]$ such that $x\neq y$ + there exist $U\in\closeds{X}$ such that + $x\in U\not\ni y$ or $x\notin U\ni y$. +\end{proposition} +\begin{proof} + Follows by \cref{kolmogorov_implies_kolmogorov_for_closeds,kolmogorov_for_closeds_implies_kolmogorov}. +\end{proof} + +% T1 separation (Fréchet topology) +\begin{definition}\label{teeone} + $X$ is \teeone\ iff + for all $x,y\in\carrier[X]$ such that $x\neq y$ + there exist $U, V\in\opens[X]$ such that + $U\ni x\notin V$ and $V\ni y\notin U$. +\end{definition} + +\begin{abbreviation}\label{teeone_space} + $X$ is a \teeone-space iff $X$ is a topological space and + $X$ is \teeone. +\end{abbreviation} + +\begin{proposition}\label{teeone_implies_singletons_closed} + Let $X$ be a \teeone-space. + Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$. +\end{proposition} +\begin{proof} + Omitted. + % TODO + % Choose for every y distinct from x and open subset U_y containing y but not x. + % The union U of all the U_y is open. + % {x} is the complement of U in \carrier[X]. +\end{proof} +% +% Conversely, if \{x\} is open, then for any y distinct from x we can use +% X\setminus\{x\} as the open neighbourhood of y. + +% T2 separation +\begin{definition}\label{is_hausdorff} + $X$ is Hausdorff iff + for all $x,y\in\carrier[X]$ such that $x\neq y$ + there exist $U, V\in\opens[X]$ such that + $x\in U$ and $y\in V$ and $U$ is disjoint from $V$. +\end{definition} + +\begin{abbreviation}\label{hausdorff_space} + $X$ is a Hausdorff space iff $X$ is a topological space and + $X$ is Hausdorff. +\end{abbreviation} + +\begin{abbreviation}\label{teetwo} + $X$ is \teetwo\ iff $X$ is Hausdorff. +\end{abbreviation} + +\begin{abbreviation}\label{teetwo_space} + $X$ is a \teetwo-space iff $X$ is a Hausdorff space. +\end{abbreviation} + +\begin{proposition}\label{teeone_space_is_teezero_space} + Let $X$ be a \teeone-space. + Then $X$ is a \teezero-space. +\end{proposition} +\begin{proof} + Follows by \cref{is_kolmogorov,teeone}. +\end{proof} + +\begin{proposition}\label{teetwo_space_is_teeone_space} + Let $X$ be a \teetwo-space. + Then $X$ is a \teeone-space. +\end{proposition} +\begin{proof} + Omitted. % TODO +\end{proof} diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex new file mode 100644 index 0000000..e467d48 --- /dev/null +++ b/library/topology/topological-space.tex @@ -0,0 +1,258 @@ +\import{set.tex} +\import{set/powerset.tex} + +\section{Topological spaces} + +\begin{struct}\label{topological_space} + A topological space $X$ is a onesorted structure equipped with + \begin{enumerate} + \item $\opens$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{opens_type} $\opens[X]$ is a family of subsets of $\carrier[X]$. + \item\label{emptyset_open} $\emptyset\in\opens[X]$. + \item\label{carrier_open} $\carrier[X]\in\opens[X]$. + \item\label{opens_inter} For all $A, B\in \opens[X]$ we have $A\inter B\in\opens[X]$. + \item\label{opens_unions} For all $F\subseteq \opens[X]$ we have $\unions{F}\in\opens[X]$. + \end{enumerate} +\end{struct} + +\begin{abbreviation}\label{is_open_in} + $U$ is open iff $U\in\opens$. +\end{abbreviation} + +\begin{abbreviation}\label{is_open} + $U$ is open in $X$ iff $U\in\opens[X]$. +\end{abbreviation} + +\begin{proposition}\label{union_open} + Let $X$ be a topological space. + Suppose $A$, $B$ are open. + Then $A\union B$ is open. +\end{proposition} +\begin{proof} + $\{A, B\}\subseteq \opens$. + $\unions{\{A, B\}}$ is open. + $\unions{\{A, B\}} = A\union B$. +\end{proof} + +\begin{definition}[Interiors]\label{interiors} + $\interiors{A}{X} = \{ U\in\opens[X]\mid U\subseteq A\}$. +\end{definition} + +\begin{definition}[Interior]\label{interior} + $\interior{A}{X} = \unions{\interiors{A}{X}}$. +\end{definition} + +\begin{proposition}[Interior]\label{interior_elem_intro} + Suppose $U\in\opens[X]$ and $a\in U\subseteq A$. + Then $a\in\interior{A}{X}$. +\end{proposition} +\begin{proof} + $U\in\interiors{A}{X}$. +\end{proof} + +\begin{proposition}[Interior]\label{interior_elem_elim} + Suppose $a\in\interior{A}{X}$. + Then there exists $U\in\opens[X]$ + such that $a\in U\subseteq A$. +\end{proposition} +\begin{proof} + Take $U\in\interiors{A}{X}$ such that $a\in U$. +\end{proof} + +\begin{proposition}[Interior]\label{interior_elem_iff} + $a\in\interior{A}{X}$ iff + there exists $U\in\opens[X]$ + such that $a\in U\subseteq A$. +\end{proposition} +\begin{proof} + Follows by \cref{interior_elem_intro,interior_elem_elim}. +\end{proof} + +\begin{proposition}\label{interior_of_open} + Let $X$ be a topological space. + Suppose $U$ is open in $X$. + Then $\interior{U}{X} = U$. +\end{proposition} +\begin{proof} + $U\in\interiors{U}{X}$. + Follows by \cref{subseteq,interior_elem_iff,neq_witness}. +\end{proof} + +\begin{proposition}\label{interior_is_open} + Let $X$ be a topological space. + Then $\interior{A}{X}$ is open. +\end{proposition} +\begin{proof} + $\interiors{A}{X}\subseteq\opens[X]$. +\end{proof} + +\begin{proposition}\label{interior_subseteq} + Then $\interior{A}{X}\subseteq A$. +\end{proposition} + +\begin{proposition}\label{interior_maximal} + Let $X$ be a topological space. + Suppose $U\subseteq A\subseteq \carrier[X]$. + Suppose $U$ is open. + Then $U\subseteq \interior{A}{X}$. +\end{proposition} + +\begin{proposition}\label{interior_eq_self_implies_open} + Let $X$ be a topological space. + Suppose $\interior{A}{X} = A$. + Then $A$ is open. +\end{proposition} + +\begin{corollary}\label{interior_eq_self_iff_open} + Let $X$ be a topological space. + Then $\interior{A}{X} = A$ iff $A$ is open in $X$. +\end{corollary} + +\begin{proposition}\label{interior_carrier} + Let $X$ be a topological space. + $\interior{\carrier[X]}{X} = \carrier[X]$. +\end{proposition} +\begin{proof} + $\carrier[X]\in\opens[X]$. + $\carrier[X]\subseteq\carrier[X]$ by \cref{subseteq_refl}. + Thus $\carrier[X]\in\interiors{\carrier[X]}{X}$ by \cref{interiors}. + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{interior_type} + Let $X$ be a topological space. + Then $\interior{A}{X}\in\pow{\carrier[X]}$. +\end{proposition} +\begin{proof} + We have $\interiors{A}{X}\subseteq \pow{\carrier[X]}$. + % As they are open subsets of X containing A + % + Thus $\interior{A}{X}\subseteq \carrier[X]$ by \cref{interior,unions_subseteq_of_powerset_is_subseteq}. +\end{proof} + +\subsection{Closed sets} + +\begin{definition}\label{is_closed_in} + $A$ is closed in $X$ iff $\carrier[X]\setminus A$ is open in $X$. +\end{definition} + +\begin{abbreviation}\label{is_clopen_in} + $A$ is clopen in $X$ iff $A$ is open in $X$ and closed in $X$. +\end{abbreviation} + +\begin{proposition}\label{emptyset_is_closed} + Let $X$ be a topological space. + Then $\emptyset$ is closed in $X$. +\end{proposition} +\begin{proof} + $\carrier[X]\setminus \emptyset = \carrier[X]$. +\end{proof} + +\begin{proposition}\label{carrier_is_closed} + Let $X$ be a topological space. + Then $\emptyset$ is closed in $X$. +\end{proposition} +\begin{proof} + $\carrier[X]\setminus \carrier[X] = \emptyset$. +\end{proof} + +\begin{definition}[Closed sets]\label{closeds} + $\closeds{X} = \{ A\in\pow{\carrier[X]}\mid\text{$A$ is closed in $X$}\}$. +\end{definition} + +\begin{proposition}\label{complement_of_open_elem_closeds} + Let $X$ be a topological space. + Let $U\in\opens[X]$. + Then $\carrier[X]\setminus U\in\closeds{X}$. +\end{proposition} +\begin{proof} + $\carrier[X]\setminus U\in\pow{\carrier[X]}$. + $U\subseteq\carrier[X]$ by \cref{opens_type}. + Hence $\carrier[X]\setminus(\carrier[X]\setminus U) = U$ by \cref{double_relative_complement}. + $\carrier[X]\setminus U$ is closed in $X$. +\end{proof} + + +\begin{definition}[Closed covers]\label{closures} + $\closures{A}{X} = \{ D\in\pow{\carrier[X]}\mid \text{$A\subseteq D$ and $D$ is closed in $X$}\}$. +\end{definition} + +\begin{definition}[Closure]\label{closure} + $\closure{A}{X} = \inters{\closures{A}{X}}$. +\end{definition} + +\begin{proposition}\label{closure_emptyset} + Let $X$ be a topological space. + Then $\closure{\emptyset}{X} = \emptyset$. +\end{proposition} +\begin{proof} + $\emptyset\in\closures{\emptyset}{X}$. +\end{proof} + +\begin{proposition}\label{closure_carrier} + Let $X$ be a topological space. + Then $\closure{\carrier[X]}{X} = \carrier[X]$. +\end{proposition} +\begin{proof} + %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\subseteq D$ by \cref{closures}. + %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\supseteq D$ by \cref{pow_iff,closures}. + %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X] = D$ by \cref{subseteq_antisymmetric}. + For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X] = D$ + by \cref{pow_iff,closures,subseteq_antisymmetric}. + Now $\carrier[X]\in\closures{\carrier[X]}{X}$. + Thus $\closures{\carrier[X]}{X} = \{\carrier[X]\}$ + by \cref{singleton_iff_inhabited_subsingleton}. + Follows by \cref{inters_singleton,closure}. +\end{proof} + + +\begin{proposition}%[Complement of interior equals closure of complement] +\label{complement_interior_eq_closure_complement} + $\carrier[X]\setminus\interior{A}{X} = \closure{(\carrier[X]\setminus A)}{X}$. +\end{proposition} +\begin{proof} + Omitted. % Use general De Morgan's Law in Pow|X| +\end{proof} + +\begin{definition}[Frontier]\label{frontier} + $\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$. +\end{definition} + + + +\begin{proposition}%[Frontier as intersection of closures] +\label{frontier_as_inter} + $\frontier{A}{X} = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. +\end{proposition} +\begin{proof} + % TODO + Omitted. + %$\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$. % by frontier (definition) + %$\closure{A}{X}\setminus\interior{A}{X} = \closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X})$. % by setminus_eq_inter_complement + %$\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X}) = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. % by complement_interior_eq_closure_complement +\end{proof} + +\begin{proposition}\label{frontier_of_emptyset} + Let $X$ be a topological space. + Then $\frontier{\emptyset}{X} = \emptyset$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{frontier_of_carrier} + Let $X$ be a topological space. + Then $\frontier{\carrier[X]}{X} = \emptyset$. +\end{proposition} +\begin{proof} + $\frontier{\carrier[X]}{X} = \carrier[X]\setminus\carrier[X]$ + by \cref{frontier,interior_carrier,closure_carrier}. + Follows by \cref{setminus_self}. +\end{proof} + +\begin{definition}\label{neighbourhoods} + $\neighbourhoods{x}{X} = \{U\in\opens[X] \mid x\in U\}$. +\end{definition} |