1
\section{Sets}\label{Sets}
3
This is a library on sets defined by their characteristic predicate.
4
It contains the following modules:
7
\item {\tt Ensembles.v}
8
\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v}
9
\item {\tt Relations\_1.v}, {\tt Relations\_2.v},
10
{\tt Relations\_3.v}, {\tt Relations\_1\_facts.v}, \\
11
{\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v}
12
\item {\tt Partial\_Order.v}, {\tt Cpo.v}
13
\item {\tt Powerset.v}, {\tt Powerset\_facts.v},
14
{\tt Powerset\_Classical\_facts.v}
15
\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v}
17
\item {\tt Infinite\_sets.v}
18
\item {\tt Integers.v}