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 25800
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 25799 . 2  class  Intvl
2 cioo 10672 . . . . 5  class  (,)
32crn 4706 . . . 4  class  ran  (,)
4 cioc 10673 . . . . . 6  class  (,]
54crn 4706 . . . . 5  class  ran  (,]
6 cico 10674 . . . . . . 7  class  [,)
76crn 4706 . . . . . 6  class  ran  [,)
8 cicc 10675 . . . . . . 7  class  [,]
98crn 4706 . . . . . 6  class  ran  [,]
107, 9cun 3163 . . . . 5  class  ( ran 
[,)  u.  ran  [,] )
115, 10cun 3163 . . . 4  class  ( ran 
(,]  u.  ( ran  [,) 
u.  ran  [,] )
)
123, 11cun 3163 . . 3  class  ( ran 
(,)  u.  ( ran  (,] 
u.  ( ran  [,)  u. 
ran  [,] ) ) )
13 cr 8752 . . . 4  class  RR
1413cpw 3638 . . 3  class  ~P RR
1512, 14cin 3164 . 2  class  ( ( ran  (,)  u.  ( ran  (,]  u.  ( ran 
[,)  u.  ran  [,] )
) )  i^i  ~P RR )
161, 15wceq 1632 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  25801  intrr  25802  intvconlem1  25806
  Copyright terms: Public domain W3C validator