aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Sets/intro.tex
blob: 83c2177fd3b49f6abddbf906cd3dd3fd6279db55 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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: