Metamath Proof Explorer


Table of Contents - 20.3.14.4. Canonical embedding of the real numbers into a complete ordered field

  1. crrh
  2. crrext
  3. df-rrh
  4. rrhval
  5. rrhcn
  6. rrhf
  7. df-rrext
  8. isrrext
  9. rrextnrg
  10. rrextdrg
  11. rrextnlm
  12. rrextchr
  13. rrextcusp
  14. rrexttps
  15. rrexthaus
  16. rrextust
  17. rerrext
  18. cnrrext
  19. qqtopn
  20. rrhfe
  21. rrhcne
  22. rrhqima
  23. rrh0