Metamath Proof Explorer


Table of Contents - 10.10.1. Definition and basic properties

  1. cpsmet
  2. cxmet
  3. cmet
  4. cbl
  5. cfbas
  6. cfg
  7. cmopn
  8. cmetu
  9. df-psmet
  10. df-xmet
  11. df-met
  12. df-bl
  13. df-mopn
  14. df-fbas
  15. df-fg
  16. df-metu
  17. ccnfld
  18. df-cnfld
  19. cnfldstr
  20. cnfldex
  21. cnfldbas
  22. cnfldadd
  23. cnfldmul
  24. cnfldcj
  25. cnfldtset
  26. cnfldle
  27. cnfldds
  28. cnfldunif
  29. cnfldfun
  30. cnfldfunALT
  31. xrsstr
  32. xrsex
  33. xrsbas
  34. xrsadd
  35. xrsmul
  36. xrstset
  37. xrsle
  38. cncrng
  39. cnring
  40. xrsmcmn
  41. cnfld0
  42. cnfld1
  43. cnfldneg
  44. cnfldplusf
  45. cnfldsub
  46. cndrng
  47. cnflddiv
  48. cnfldinv
  49. cnfldmulg
  50. cnfldexp
  51. cnsrng
  52. xrsmgm
  53. xrsnsgrp
  54. xrsmgmdifsgrp
  55. xrs1mnd
  56. xrs10
  57. xrs1cmn
  58. xrge0subm
  59. xrge0cmn
  60. xrsds
  61. xrsdsval
  62. xrsdsreval
  63. xrsdsreclblem
  64. xrsdsreclb
  65. cnsubmlem
  66. cnsubglem
  67. cnsubrglem
  68. cnsubdrglem
  69. qsubdrg
  70. zsubrg
  71. gzsubrg
  72. nn0subm
  73. rege0subm
  74. absabv
  75. zsssubrg
  76. qsssubdrg
  77. cnsubrg
  78. cnmgpabl
  79. cnmgpid
  80. cnmsubglem
  81. rpmsubg
  82. gzrngunitlem
  83. gzrngunit
  84. gsumfsum
  85. regsumfsum
  86. expmhm
  87. nn0srg
  88. rge0srg