| author | nipkow |
| Mon, 01 Jul 2002 12:50:35 +0200 | |
| changeset 13261 | a0460a450cf9 |
| parent 12254 | 78bc1f3462b5 |
| child 14631 | ec1e67f88f49 |
| permissions | -rw-r--r-- |
| 10755 | 1 |
<!-- $Id$ --> |
2 |
<HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY> |
|
3 |
||
4 |
<H2>Hyperreal--Ultrafilter Construction of the Non-Standard Reals</H2> |
|
| 12254 | 5 |
See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real |
6 |
Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190. |
|
| 10755 | 7 |
|
8 |
<UL> |
|
9 |
<LI><A HREF="Zorn.html">Zorn</A> |
|
|
11544
97305ee424a9
HOL-Real-Hyperreal made a plain session (no longer an image);
wenzelm
parents:
10755
diff
changeset
|
10 |
Zorn's Lemma: proof based on the ZF version. |
| 10755 | 11 |
|
12 |
<LI><A HREF="Filter.html">Filter</A> |
|
13 |
Theory of Filters and Ultrafilters. |
|
14 |
Main result is a version of the Ultrafilter Theorem proved using |
|
15 |
Zorn's Lemma. |
|
16 |
||
17 |
<LI><A HREF="HyperDef.html">HyperDef</A> |
|
18 |
Ultrapower construction of the hyperreals |
|
19 |
||
20 |
<LI><A HREF="NSA.html">NSA</A> |
|
21 |
Theory defining sets of infinite numbers, infinitesimals, |
|
22 |
the infinitely close relation, and their various algebraic properties. |
|
23 |
||
24 |
<LI><A HREF="HyperNat.html">HyperNat</A> |
|
25 |
Ultrapower construction of the hypernaturals |
|
26 |
||
27 |
<LI><A HREF="HyperPow.html">HyperPow</A> |
|
28 |
Powers theory for the hyperreals |
|
29 |
||
30 |
<LI><A HREF="Star.html">Star</A> |
|
31 |
Nonstandard extensions of real sets and real functions |
|
32 |
||
33 |
<LI><A HREF="NatStar.html">NatStar</A> |
|
34 |
Nonstandard extensions of sets of naturals and functions on the natural |
|
35 |
numbers |
|
36 |
||
37 |
<LI><A HREF="SEQ.html">SEQ</A> |
|
38 |
Theory of sequences developed using standard and nonstandard analysis |
|
39 |
||
40 |
<LI><A HREF="Lim.html">Lim</A> |
|
41 |
Theory of limits, continuous functions, and derivatives |
|
42 |
||
43 |
<LI><A HREF="Series.html">Series</A> |
|
44 |
Standard theory of finite summation and infinite series |
|
45 |
||
46 |
</UL> |
|
47 |
||
48 |
<P>Last modified on $Date$ |
|
49 |
||
50 |
<HR> |
|
51 |
||
52 |
<ADDRESS> |
|
53 |
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
|
54 |
</ADDRESS> |
|
55 |
</BODY></HTML> |