Metamath Proof Explorer

Definition df-liminf

Description: Define the inferior limit of a sequence of extended real numbers. (Contributed by GS, 2-Jan-2022)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsi 
 |-  liminf
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 cinf 
 |-  inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < )
15 3 4 14 cmpt 
 |-  ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
16 15 crn 
 |-  ran ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
17 16 11 13 csup 
 |-  sup ( ran ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < )
18 1 2 17 cmpt 
 |-  ( x e. _V |-> sup ( ran ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
19 0 18 wceq 
 |-  liminf = ( x e. _V |-> sup ( ran ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )