diff options
Diffstat (limited to 'theories/Sets/intro.tex')
| -rwxr-xr-x | theories/Sets/intro.tex | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex new file mode 100755 index 00000000..83c2177f --- /dev/null +++ b/theories/Sets/intro.tex @@ -0,0 +1,24 @@ +\section{Sets}\label{Sets} + +This is a library on sets defined by their characteristic predicate. +It contains the following modules: + +\begin{itemize} +\item {\tt Ensembles.v} +\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v} +\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, + {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v}, \\ + {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v} +\item {\tt Partial\_Order.v}, {\tt Cpo.v} +\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, + {\tt Powerset\_Classical\_facts.v} +\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v} +\item {\tt Image.v} +\item {\tt Infinite\_sets.v} +\item {\tt Integers.v} +\end{itemize} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: |