Metamath Proof Explorer


Table of Contents - 12.4.8. Normed algebraic structures

In the following, the norm of a normed algebraic structure (group, left module, vector space) is defined by the (given) distance function (the norm of an element is its distance from the zero element, see nmval: ). By this definition, the norm function is actually a norm (satisfying the properties of being a function into the reals, subadditivity/triangle inequality , absolute homogeneity ( n(sx) = |s| n(x) ) [Remark: for group norms, some authors (e.g. Juris Steprans in "A characterization of free abelian groups") demand that n(sx) = |s| n(x) for all s in ZZ, whereas other authors (e.g. N. H. Bingham and A. J. Ostaszewski in "Normed versus topological groups: Dichotomy and duality") only require inversion symmetry, i.e. n(-x) = n(x). The definition df-ngp of a group norm follows the second aproach, see nminv.] and positive definiteness/point-separating ( n(x) = 0 <-> x = 0 ) if the structure is a metric space with a right-translation-invariant metric (see nmf, nmtri, nmvs and nmeq0). An alternate definition of a normed group (i.e. a group equipped with a norm) without using the properties of a metric space is given by theorem tngngp3. For a structure being a group, the (arbitrary) distance function can be restricted to the elements of the group without affecting the norm, see nmfval2.

Usually, however, the norm of a normed structure is given, and the corresponding metric ("induced metric") is achieved by defining a distance function based on the norm (the distance between two elements is the norm of their difference, see ngpds: ). The operation does exactly this, i.e. it adds a distance function (and a topology) to a structure (which should be at least a group) corresponding to a given norm in the just shown way: , see also tngds. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2) resp. if the norm is in fact a norm (see tngngpd). If the norm is derived from a given metric, as done with df-nm, the induced metric is the original metric restricted to the base set: , see nrmtngdist, and the norm remains the same: , see nrmtngnrm.

  1. cnm
  2. cngp
  3. ctng
  4. cnrg
  5. cnlm
  6. cnvc
  7. df-nm
  8. df-ngp
  9. df-tng
  10. df-nrg
  11. df-nlm
  12. df-nvc
  13. nmfval
  14. nmval
  15. nmfval2
  16. nmval2
  17. nmf2
  18. nmpropd
  19. nmpropd2
  20. isngp
  21. isngp2
  22. isngp3
  23. ngpgrp
  24. ngpms
  25. ngpxms
  26. ngptps
  27. ngpmet
  28. ngpds
  29. ngpdsr
  30. ngpds2
  31. ngpds2r
  32. ngpds3
  33. ngpds3r
  34. ngprcan
  35. ngplcan
  36. isngp4
  37. ngpinvds
  38. ngpsubcan
  39. nmf
  40. nmcl
  41. nmge0
  42. nmeq0
  43. nmne0
  44. nmrpcl
  45. nminv
  46. nmmtri
  47. nmsub
  48. nmrtri
  49. nm2dif
  50. nmtri
  51. nmtri2
  52. ngpi
  53. nm0
  54. nmgt0
  55. sgrim
  56. sgrimval
  57. subgnm
  58. subgnm2
  59. subgngp
  60. ngptgp
  61. ngppropd
  62. reldmtng
  63. tngval
  64. tnglem
  65. tngbas
  66. tngplusg
  67. tng0
  68. tngmulr
  69. tngsca
  70. tngvsca
  71. tngip
  72. tngds
  73. tngtset
  74. tngtopn
  75. tngnm
  76. tngngp2
  77. tngngpd
  78. tngngp
  79. tnggrpr
  80. tngngp3
  81. nrmtngdist
  82. nrmtngnrm
  83. tngngpim
  84. isnrg
  85. nrgabv
  86. nrgngp
  87. nrgring
  88. nmmul
  89. nrgdsdi
  90. nrgdsdir
  91. nm1
  92. unitnmn0
  93. nminvr
  94. nmdvr
  95. nrgdomn
  96. nrgtgp
  97. subrgnrg
  98. tngnrg
  99. isnlm
  100. nmvs
  101. nlmngp
  102. nlmlmod
  103. nlmnrg
  104. nlmngp2
  105. nlmdsdi
  106. nlmdsdir
  107. nlmmul0or
  108. sranlm
  109. nlmvscnlem2
  110. nlmvscnlem1
  111. nlmvscn
  112. rlmnlm
  113. rlmnm
  114. nrgtrg
  115. nrginvrcnlem
  116. nrginvrcn
  117. nrgtdrg
  118. nlmtlm
  119. isnvc
  120. nvcnlm
  121. nvclvec
  122. nvclmod
  123. isnvc2
  124. nvctvc
  125. lssnlm
  126. lssnvc
  127. rlmnvc
  128. ngpocelbl