Metamath Proof Explorer
Table of Contents - 20.3.14.4. Canonical embedding of the real numbers into a complete ordered field
- crrh
- crrext
- df-rrh
- rrhval
- rrhcn
- rrhf
- df-rrext
- isrrext
- rrextnrg
- rrextdrg
- rrextnlm
- rrextchr
- rrextcusp
- rrexttps
- rrexthaus
- rrextust
- rerrext
- cnrrext
- qqtopn
- rrhfe
- rrhcne
- rrhqima
- rrh0