Metamath Proof Explorer

Definition df-limsup

Description: Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of Gleason p. 175. See limsupval for its value. (Contributed by NM, 26-Oct-2005) (Revised by AV, 11-Sep-2020)

Ref Expression
Assertion df-limsup 
|- limsup = ( x e. _V |-> inf ( ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsp 
 |-  limsup
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vk 
 |-  k
4 cr 
 |-  RR
5 1 cv 
 |-  x
6 3 cv 
 |-  k
7 cico 
 |-  [,)
8 cpnf 
 |-  +oo
9 6 8 7 co 
 |-  ( k [,) +oo )
10 5 9 cima 
 |-  ( x " ( k [,) +oo ) )
11 cxr 
 |-  RR*
12 10 11 cin 
 |-  ( ( x " ( k [,) +oo ) ) i^i RR* )
13 clt 
 |-  <
14 12 11 13 csup 
 |-  sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < )
15 3 4 14 cmpt 
 |-  ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
16 15 crn 
 |-  ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
17 16 11 13 cinf 
 |-  inf ( ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < )
18 1 2 17 cmpt 
 |-  ( x e. _V |-> inf ( ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
19 0 18 wceq 
 |-  limsup = ( x e. _V |-> inf ( ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )