src/HOL/Real/Hyperreal/README.html
changeset 5981 ec5c3d17969f
parent 5979 11cbf236ca16
child 10043 a0364652e115
equal deleted inserted replaced
5980:2e9314c07146 5981:ec5c3d17969f
     3 
     3 
     4 <H2>Hyperreal--Ultrafilter Construction of the Non-Standard Reals</H2>
     4 <H2>Hyperreal--Ultrafilter Construction of the Non-Standard Reals</H2>
     5 
     5 
     6 <UL>
     6 <UL>
     7 <LI><A HREF="Zorn.html">Zorn</A>
     7 <LI><A HREF="Zorn.html">Zorn</A>
     8 Zorn's Lemma: proof based on the <A HREF="../../ZF/Zorn.html">ZF version</A>
     8 Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A>
     9 
     9 
    10 <LI><A HREF="Filter.html">Filter</A>
    10 <LI><A HREF="Filter.html">Filter</A>
    11 Theory of Filters and Ultrafilters.
    11 Theory of Filters and Ultrafilters.
    12 Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
    12 Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
    13 </UL>
    13 </UL>