Definition df-limsup 15507

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

Assertion

Ref	Expression
df-limsup	⊢ lim sup = (𝑥 ∈ V ↦ inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))

Distinct variable group:   𝑥,𝑘

Detailed syntax breakdown of Definition df-limsup

Step	Hyp	Ref	Expression
1		clsp 15506	. 2 class lim sup
2		vx	. . 3 setvar 𝑥
3		cvv 3480	. . 3 class V
4		vk	. . . . . 6 setvar 𝑘
5		cr 11154	. . . . . 6 class ℝ
6	2	cv 1539	. . . . . . . . 9 class 𝑥
7	4	cv 1539	. . . . . . . . . 10 class 𝑘
8		cpnf 11292	. . . . . . . . . 10 class +∞
9		cico 13389	. . . . . . . . . 10 class [,)
10	7, 8, 9	co 7431	. . . . . . . . 9 class (𝑘[,)+∞)
11	6, 10	cima 5688	. . . . . . . 8 class (𝑥 “ (𝑘[,)+∞))
12		cxr 11294	. . . . . . . 8 class ℝ*
13	11, 12	cin 3950	. . . . . . 7 class ((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*)
14		clt 11295	. . . . . . 7 class <
15	13, 12, 14	csup 9480	. . . . . 6 class sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )
16	4, 5, 15	cmpt 5225	. . . . 5 class (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
17	16	crn 5686	. . . 4 class ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
18	17, 12, 14	cinf 9481	. . 3 class inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < )
19	2, 3, 18	cmpt 5225	. 2 class (𝑥 ∈ V ↦ inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
20	1, 19	wceq 1540	1 wff lim sup = (𝑥 ∈ V ↦ inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))

This definition is referenced by:  limsupcl  15509  limsupval  15510