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	⊢ lim sup = ( 𝑥 ∈ V ↦ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clsp	⊢ lim sup
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vk	⊢ 𝑘
4		cr	⊢ ℝ
5	1	cv	⊢ 𝑥
6	3	cv	⊢ 𝑘
7		cico	⊢ [,)
8		cpnf	⊢ +∞
9	6 8 7	co	⊢ ( 𝑘 [,) +∞ )
10	5 9	cima	⊢ ( 𝑥 “ ( 𝑘 [,) +∞ ) )
11		cxr	⊢ ℝ*
12	10 11	cin	⊢ ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* )
13		clt	⊢ <
14	12 11 13	csup	⊢ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < )
15	3 4 14	cmpt	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
16	15	crn	⊢ ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
17	16 11 13	cinf	⊢ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < )
18	1 2 17	cmpt	⊢ ( 𝑥 ∈ V ↦ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
19	0 18	wceq	⊢ lim sup = ( 𝑥 ∈ V ↦ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )