|
14631
|
1 |
<HTML><HEAD><TITLE>HOL/Complex/README</TITLE>
|
|
|
2 |
<meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
|
|
|
3 |
</HEAD><BODY>
|
|
14005
|
4 |
|
|
14631
|
5 |
<H1>Complex: The Complex Numbers</H1>
|
|
|
6 |
<P>This directory defines the type <KBD>complex</KBD> of the complex numbers,
|
|
14005
|
7 |
with numeric constants and some complex analysis. The development includes
|
|
|
8 |
nonstandard analysis for the complex numbers. Note that the image
|
|
14020
|
9 |
<KBD>HOL-Complex</KBD> includes theories from the directories
|
|
14631
|
10 |
<KBD><a href="../Real/">HOL/Real</a></KBD> and <KBD><a href="../Hyperreal/">HOL/Hyperreal</a></KBD>.
|
|
|
11 |
|
|
14005
|
12 |
|
|
14631
|
13 |
<ul>
|
|
|
14 |
<li><a href="CLim.html">CLim</a> Limits, continuous functions, and derivatives for the complex numbers
|
|
|
15 |
<li><a href="CSeries.html">CSeries</a> Finite summation and infinite series for the complex numbers
|
|
|
16 |
<li><a href="CStar.html">CStar</a> Star-transforms for the complex numbers, to form non-standard extensions of sets and functions
|
|
|
17 |
<li><a href="Complex.html">Complex</a> The complex numbers
|
|
|
18 |
<li><a href="NSCA.html">NSCA</a> Nonstandard complex analysis
|
|
|
19 |
<li><a href="NSComplex.html">NSComplex</a> Ultrapower construction of the nonstandard complex numbers
|
|
|
20 |
<li><a href="NSInduct.html">NSInduct</a> Nonstandard induction for the hypernatural numbers
|
|
|
21 |
</ul>
|
|
|
22 |
<HR>
|
|
14005
|
23 |
<P>Last modified $Date$
|
|
|
24 |
|
|
|
25 |
</HTML>
|