Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Extended real and complex numbers, real and complex projective lines
Extended numbers and projective lines as sets
df-bj-rrhat
Next ⟩
bj-rrhatsscchat
Metamath Proof Explorer
Ascii
Unicode
Definition
df-bj-rrhat
Description:
Define the real projective line.
(Contributed by
BJ
, 27-Jun-2019)
Ref
Expression
Assertion
df-bj-rrhat
⊢
ℝ
^
=
ℝ
∪
∞
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
crrhat
class
ℝ
^
1
cr
class
ℝ
2
cinfty
class
∞
3
2
csn
class
∞
4
1
3
cun
class
ℝ
∪
∞
5
0
4
wceq
wff
ℝ
^
=
ℝ
∪
∞