Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-intvl Unicode version

Definition df-intvl 25697
Description: The intervals of  RR. (Contributed by FL, 29-May-2014.)
Assertion
Ref Expression
df-intvl  |-  Intvl  =  ( ( ran  (,)  u.  ( ran  (,]  u.  ( ran  [,)  u.  ran  [,] ) ) )  i^i 
~P RR )

Detailed syntax breakdown of Definition df-intvl
StepHypRef Expression
1 cintvl 25696 . 2  class  Intvl
2 cioo 10656 . . . . 5  class  (,)
32crn 4690 . . . 4  class  ran  (,)
4 cioc 10657 . . . . . 6  class  (,]
54crn 4690 . . . . 5  class  ran  (,]
6 cico 10658 . . . . . . 7  class  [,)
76crn 4690 . . . . . 6  class  ran  [,)
8 cicc 10659 . . . . . . 7  class  [,]
98crn 4690 . . . . . 6  class  ran  [,]
107, 9cun 3150 . . . . 5  class  ( ran 
[,)  u.  ran  [,] )
115, 10cun 3150 . . . 4  class  ( ran 
(,]  u.  ( ran  [,) 
u.  ran  [,] )
)
123, 11cun 3150 . . 3  class  ( ran 
(,)  u.  ( ran  (,] 
u.  ( ran  [,)  u. 
ran  [,] ) ) )
13 cr 8736 . . . 4  class  RR
1413cpw 3625 . . 3  class  ~P RR
1512, 14cin 3151 . 2  class  ( ( ran  (,)  u.  ( ran  (,]  u.  ( ran 
[,)  u.  ran  [,] )
) )  i^i  ~P RR )
161, 15wceq 1623 1  wff  Intvl  =  ( ( ran  (,)  u.  ( ran  (,]  u.  ( ran  [,)  u.  ran  [,] ) ) )  i^i 
~P RR )
Colors of variables: wff set class
This definition is referenced by:  intvlset  25698  intrr  25699  intvconlem1  25703
  Copyright terms: Public domain W3C validator