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: 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 , 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., . The definition df-ngp of a group norm follows the second approach, see nminv.] and positive definiteness/point-separation ) 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) not using the properties of a metric space is given by Theorem tngngp3. The norm can be expressed as the distance to zero (nmfval), so in a structure with a zero (a "pointed set", for instance a monoid or a group), the norm can be expressed as the distance restricted to the elements of the base set to zero (nmfval0).

Usually, however, the norm of a normed structure is given, and the corresponding metric ("induced metric") is defined as the 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 for the difference of two elements to make sense) corresponding to a given norm as explained above: , see also tngds. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2) or 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. nmfval0
  16. nmfval2
  17. nmval2
  18. nmf2
  19. nmpropd
  20. nmpropd2
  21. isngp
  22. isngp2
  23. isngp3
  24. ngpgrp
  25. ngpms
  26. ngpxms
  27. ngptps
  28. ngpmet
  29. ngpds
  30. ngpdsr
  31. ngpds2
  32. ngpds2r
  33. ngpds3
  34. ngpds3r
  35. ngprcan
  36. ngplcan
  37. isngp4
  38. ngpinvds
  39. ngpsubcan
  40. nmf
  41. nmcl
  42. nmge0
  43. nmeq0
  44. nmne0
  45. nmrpcl
  46. nminv
  47. nmmtri
  48. nmsub
  49. nmrtri
  50. nm2dif
  51. nmtri
  52. nmtri2
  53. ngpi
  54. nm0
  55. nmgt0
  56. sgrim
  57. sgrimval
  58. subgnm
  59. subgnm2
  60. subgngp
  61. ngptgp
  62. ngppropd
  63. reldmtng
  64. tngval
  65. tnglem
  66. tngbas
  67. tngplusg
  68. tng0
  69. tngmulr
  70. tngsca
  71. tngvsca
  72. tngip
  73. tngds
  74. tngtset
  75. tngtopn
  76. tngnm
  77. tngngp2
  78. tngngpd
  79. tngngp
  80. tnggrpr
  81. tngngp3
  82. nrmtngdist
  83. nrmtngnrm
  84. tngngpim
  85. isnrg
  86. nrgabv
  87. nrgngp
  88. nrgring
  89. nmmul
  90. nrgdsdi
  91. nrgdsdir
  92. nm1
  93. unitnmn0
  94. nminvr
  95. nmdvr
  96. nrgdomn
  97. nrgtgp
  98. subrgnrg
  99. tngnrg
  100. isnlm
  101. nmvs
  102. nlmngp
  103. nlmlmod
  104. nlmnrg
  105. nlmngp2
  106. nlmdsdi
  107. nlmdsdir
  108. nlmmul0or
  109. sranlm
  110. nlmvscnlem2
  111. nlmvscnlem1
  112. nlmvscn
  113. rlmnlm
  114. rlmnm
  115. nrgtrg
  116. nrginvrcnlem
  117. nrginvrcn
  118. nrgtdrg
  119. nlmtlm
  120. isnvc
  121. nvcnlm
  122. nvclvec
  123. nvclmod
  124. isnvc2
  125. nvctvc
  126. lssnlm
  127. lssnvc
  128. rlmnvc
  129. ngpocelbl