Definition df-limsup 14202

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

Assertion

Ref	Expression
df-limsup	|- limsup = ( x e. _V |-> inf ( 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

Step	Hyp	Ref	Expression
1		clsp 14201	. 2 class limsup
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vk	. . . . . 6 setvar k
5		cr 9935	. . . . . 6 class RR
6	2	cv 1482	. . . . . . . . 9 class x
7	4	cv 1482	. . . . . . . . . 10 class k
8		cpnf 10071	. . . . . . . . . 10 class +oo
9		cico 12177	. . . . . . . . . 10 class [,)
10	7, 8, 9	co 6650	. . . . . . . . 9 class ( k [,) +oo )
11	6, 10	cima 5117	. . . . . . . 8 class ( x " ( k [,) +oo ) )
12		cxr 10073	. . . . . . . 8 class RR*
13	11, 12	cin 3573	. . . . . . 7 class ( ( x " ( k [,) +oo ) ) i^i RR* )
14		clt 10074	. . . . . . 7 class <
15	13, 12, 14	csup 8346	. . . . . 6 class sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < )
16	4, 5, 15	cmpt 4729	. . . . 5 class ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
17	16	crn 5115	. . . 4 class ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
18	17, 12, 14	cinf 8347	. . 3 class inf ( ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < )
19	2, 3, 18	cmpt 4729	. 2 class ( x e. _V |-> inf ( ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
20	1, 19	wceq 1483	1 wff limsup = ( x e. _V |-> inf ( ran ( k e. RR |-> sup ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )

This definition is referenced by:  limsupcl  14204  limsupval  14205