Metamath Proof Explorer


Table of Contents - 20.16.6. Extended real and complex numbers, real and complex projective lines

In this section, we indroduce several supersets of the set of real numbers and the set of complex numbers.

Once they are given their usual topologies, which are locally compact, both topological spaces have a one-point compactification. They are denoted by and respectively, defined in df-bj-cchat and df-bj-rrhat, and the point at infinity is denoted by , defined in df-bj-infty.

Both and also have "directional compactifications", denoted respectively by , defined in df-bj-rrbar (already defined as , see df-xr) and , defined in df-bj-ccbar.

Since does not seem to be standard, we describe it in some detail. It is obtained by adding to a "point at infinity at the end of each ray with origin at 0". Although is not an important object in itself, the motivation for introducing it is to provide a common superset to both and and to define algebraic operations (addition, opposite, multiplication, inverse) as widely as reasonably possible.

Mathematically, is the quotient of by the diagonal multiplicative action of (think of the closed "northern hemisphere" in ^3 identified with , that each open ray from 0 included in the closed northern half-space intersects exactly once).

Since in set.mm, we want to have a genuine inclusion , we instead define as the (disjoint) union of with a circle at infinity denoted by . To have a genuine inclusion , we define and as certain points in .

Thanks to this framework, one has the genuine inclusions and and similarly and . Furthermore, one has as well as and .

Furthermore, we define the main algebraic operations on , which is not very mathematical, but "overloads" the operations, so that one can use the same notation in all cases.

  1. Complements on class abstractions of ordered pairs and binary relations
    1. bj-nfald
    2. bj-nfexd
    3. copsex2d
    4. copsex2b
    5. opelopabd
    6. opelopabb
    7. opelopabbv
    8. bj-opelrelex
    9. bj-opelresdm
    10. bj-brresdm
    11. brabd0
    12. brabd
    13. bj-brab2a1
  2. Identity relation (complements)
    1. bj-opabssvv
    2. bj-funidres
    3. bj-opelidb
    4. bj-opelidb1
    5. bj-inexeqex
    6. bj-elsn0
    7. bj-opelid
    8. bj-ideqg
    9. bj-ideqgALT
    10. bj-ideqb
    11. bj-idres
    12. bj-opelidres
    13. bj-idreseq
    14. bj-idreseqb
    15. bj-ideqg1
    16. bj-ideqg1ALT
    17. bj-opelidb1ALT
    18. bj-elid3
    19. bj-elid4
    20. bj-elid5
    21. bj-elid6
    22. bj-elid7
  3. Functionalized identity (diagonal in a Cartesian square)
    1. cdiag2
    2. df-bj-diag
    3. bj-diagval
    4. bj-diagval2
    5. bj-eldiag
    6. bj-eldiag2
  4. Direct image and inverse image
    1. cimdir
    2. df-imdir
    3. bj-imdirvallem
    4. bj-imdirval
    5. bj-imdirval2lem
    6. bj-imdirval2
    7. bj-imdirval3
    8. bj-imdiridlem
    9. bj-imdirid
    10. bj-opelopabid
    11. bj-opabco
    12. bj-xpcossxp
    13. bj-imdirco
    14. ciminv
    15. df-iminv
    16. bj-iminvval
    17. bj-iminvval2
    18. bj-iminvid
  5. Extended numbers and projective lines as sets
    1. cfractemp
    2. df-bj-fractemp
    3. cinftyexpitau
    4. df-bj-inftyexpitau
    5. cccinftyN
    6. df-bj-ccinftyN
    7. bj-inftyexpitaufo
    8. chalf
    9. df-bj-onehalf
    10. bj-inftyexpitaudisj
    11. cinftyexpi
    12. df-bj-inftyexpi
    13. bj-inftyexpiinv
    14. bj-inftyexpiinj
    15. bj-inftyexpidisj
    16. cccinfty
    17. df-bj-ccinfty
    18. bj-ccinftydisj
    19. bj-elccinfty
    20. cccbar
    21. df-bj-ccbar
    22. bj-ccssccbar
    23. bj-ccinftyssccbar
    24. cpinfty
    25. df-bj-pinfty
    26. bj-pinftyccb
    27. bj-pinftynrr
    28. cminfty
    29. df-bj-minfty
    30. bj-minftyccb
    31. bj-minftynrr
    32. bj-pinftynminfty
    33. crrbar
    34. df-bj-rrbar
    35. cinfty
    36. df-bj-infty
    37. ccchat
    38. df-bj-cchat
    39. crrhat
    40. df-bj-rrhat
    41. bj-rrhatsscchat
  6. Addition and opposite
    1. caddcc
    2. df-bj-addc
    3. coppcc
    4. df-bj-oppc
  7. Order relation on the extended reals
    1. cltxr
    2. df-bj-lt
  8. Argument, multiplication and inverse
    1. carg
    2. df-bj-arg
    3. cmulc
    4. df-bj-mulc
    5. cinvc
    6. df-bj-invc
  9. The canonical bijection from the finite ordinals
    1. ciomnn
    2. df-bj-iomnn
    3. bj-imafv
    4. bj-funun
    5. bj-fununsn1
    6. bj-fununsn2
    7. bj-fvsnun1
    8. bj-fvsnun2
    9. bj-fvmptunsn1
    10. bj-fvmptunsn2
    11. bj-iomnnom
  10. Divisibility
    1. cnnbar
    2. df-bj-nnbar
    3. czzbar
    4. df-bj-zzbar
    5. czzhat
    6. df-bj-zzhat
    7. cdivc
    8. df-bj-divc