Metamath Proof Explorer


Table of Contents - 5.4.8. Extended nonnegative integers

The function values of the hash (set size) function are either nonnegative integers or positive infinity, see hashf. To avoid the need to distinguish between finite and infinite sets (and therefore if the set size is a nonnegative integer or positive infinity), it is useful to provide a definition of the set of nonnegative integers extended by positive infinity, analogously to the extension of the real numbers , see df-xr. The definition of extended nonnegative integers can be used in Ramsey theory, because the Ramsey number is either a nonnegative integer or plus infinity, see ramcl2, or for the degree of polynomials, see mdegcl, or for the degree of vertices in graph theory, see vtxdgf.

  1. cxnn0
  2. df-xnn0
  3. elxnn0
  4. nn0ssxnn0
  5. nn0xnn0
  6. xnn0xr
  7. 0xnn0
  8. pnf0xnn0
  9. nn0nepnf
  10. nn0xnn0d
  11. nn0nepnfd
  12. xnn0nemnf
  13. xnn0xrnemnf
  14. xnn0nnn0pnf