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:
|
