Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-cchat Structured version   Visualization version   GIF version

Definition df-bj-cchat 36768
Description: Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.)
Assertion
Ref Expression
df-bj-cchat ℂ̂ = (ℂ ∪ {∞})

Detailed syntax breakdown of Definition df-bj-cchat
StepHypRef Expression
1 ccchat 36767 . 2 class ℂ̂
2 cc 11134 . . 3 class
3 cinfty 36765 . . . 4 class
43csn 4624 . . 3 class {∞}
52, 4cun 3938 . 2 class (ℂ ∪ {∞})
61, 5wceq 1533 1 wff ℂ̂ = (ℂ ∪ {∞})
Colors of variables: wff setvar class
This definition is referenced by:  bj-rrhatsscchat  36771
  Copyright terms: Public domain W3C validator