Metamath Proof Explorer
Table of Contents - 15.1.5. Full-Eta Property
The theorems in this section are derived from "A clean way to separate sets
of surreals" by Paolo Lipparini,
https://doi.org/10.48550/arXiv.1712.03500.
- bdayimaon
- nolt02olem
- nolt02o
- nogt01o
- noresle
- nomaxmo
- nominmo
- nosupprefixmo
- noinfprefixmo
- nosupcbv
- nosupno
- nosupdm
- nosupbday
- nosupfv
- nosupres
- nosupbnd1lem1
- nosupbnd1lem2
- nosupbnd1lem3
- nosupbnd1lem4
- nosupbnd1lem5
- nosupbnd1lem6
- nosupbnd1
- nosupbnd2lem1
- nosupbnd2
- noinfcbv
- noinfno
- noinfdm
- noinfbday
- noinffv
- noinfres
- noinfbnd1lem1
- noinfbnd1lem2
- noinfbnd1lem3
- noinfbnd1lem4
- noinfbnd1lem5
- noinfbnd1lem6
- noinfbnd1
- noinfbnd2lem1
- noinfbnd2
- nosupinfsep
- noetasuplem1
- noetasuplem2
- noetasuplem3
- noetasuplem4
- noetainflem1
- noetainflem2
- noetainflem3
- noetainflem4
- noetalem1
- noetalem2
- noeta