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