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

Definition df-bj-rrbar 32293
Description: Definition of the set of extended real numbers ℝ̅. See df-xr 9957. (Contributed by BJ, 29-Jun-2019.)
Assertion
Ref Expression
df-bj-rrbar ℝ̅ = (ℝ ∪ {-∞, +∞})

Detailed syntax breakdown of Definition df-bj-rrbar
StepHypRef Expression
1 crrbar 32292 . 2 class ℝ̅
2 cr 9814 . . 3 class
3 cminfty 32287 . . . 4 class -∞
4 cpinfty 32283 . . . 4 class +∞
53, 4cpr 4127 . . 3 class {-∞, +∞}
62, 5cun 3538 . 2 class (ℝ ∪ {-∞, +∞})
71, 6wceq 1475 1 wff ℝ̅ = (ℝ ∪ {-∞, +∞})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator