MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-limsup Unicode version

Definition df-limsup 11875
Description: Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 11878 for its value. (Contributed by NM, 26-Oct-2005.)
Assertion
Ref Expression
df-limsup  |-  limsup  =  ( x  e.  _V  |->  sup ( ran  (  k  e.  RR  |->  sup (
( ( x "
( k [,)  +oo ) )  i^i  RR* ) ,  RR* ,  <  ) ) ,  RR* ,  `'  <  ) )
Distinct variable group:    x, k

Detailed syntax breakdown of Definition df-limsup
StepHypRef Expression
1 clsp 11874 . 2  class  limsup
2 vx . . 3  set  x
3 cvv 2740 . . 3  class  _V
4 vk . . . . . 6  set  k
5 cr 8669 . . . . . 6  class  RR
62cv 1618 . . . . . . . . 9  class  x
74cv 1618 . . . . . . . . . 10  class  k
8 cpnf 8797 . . . . . . . . . 10  class  +oo
9 cico 10589 . . . . . . . . . 10  class  [,)
107, 8, 9co 5757 . . . . . . . . 9  class  ( k [,)  +oo )
116, 10cima 4629 . . . . . . . 8  class  ( x
" ( k [,) 
+oo ) )
12 cxr 8799 . . . . . . . 8  class  RR*
1311, 12cin 3093 . . . . . . 7  class  ( ( x " ( k [,)  +oo ) )  i^i  RR* )
14 clt 8800 . . . . . . 7  class  <
1513, 12, 14csup 7126 . . . . . 6  class  sup (
( ( x "
( k [,)  +oo ) )  i^i  RR* ) ,  RR* ,  <  )
164, 5, 15cmpt 4017 . . . . 5  class  ( k  e.  RR  |->  sup (
( ( x "
( k [,)  +oo ) )  i^i  RR* ) ,  RR* ,  <  ) )
1716crn 4627 . . . 4  class  ran  ( 
k  e.  RR  |->  sup ( ( ( x
" ( k [,) 
+oo ) )  i^i  RR* ) ,  RR* ,  <  ) )
1814ccnv 4625 . . . 4  class  `'  <
1917, 12, 18csup 7126 . . 3  class  sup ( ran  (  k  e.  RR  |->  sup ( ( ( x " ( k [,)  +oo ) )  i^i  RR* ) ,  RR* ,  <  ) ) ,  RR* ,  `'  <  )
202, 3, 19cmpt 4017 . 2  class  ( x  e.  _V  |->  sup ( ran  (  k  e.  RR  |->  sup ( ( ( x " ( k [,)  +oo ) )  i^i  RR* ) ,  RR* ,  <  ) ) ,  RR* ,  `'  <  ) )
211, 20wceq 1619 1  wff  limsup  =  ( x  e.  _V  |->  sup ( ran  (  k  e.  RR  |->  sup (
( ( x "
( k [,)  +oo ) )  i^i  RR* ) ,  RR* ,  <  ) ) ,  RR* ,  `'  <  ) )
Colors of variables: wff set class
This definition is referenced by:  limsupcl  11877  limsupval  11878
  Copyright terms: Public domain W3C validator