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 = (x \in V ⟼ inf (ran (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clsp	$class lim sup$
1		vx	$setvar x$
2		cvv	$class V$
3		vk	$setvar k$
4		cr	$class ℝ$
5	1	cv	$setvar x$
6	3	cv	$setvar k$
7		cico	$class [.)$
8		cpnf	$class +∞$
9	6 8 7	co	$class [k, +∞)$
10	5 9	cima	$class x [[k, +∞)]$
11		cxr	$class ℝ^{*}$
12	10 11	cin	$class (x [[k, +∞)] \cap ℝ^{*})$
13		clt	$class <$
14	12 11 13	csup	$class sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
15	3 4 14	cmpt	$class (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
16	15	crn	$class ran (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
17	16 11 13	cinf	$class inf (ran (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
18	1 2 17	cmpt	$class (x \in V ⟼ inf (ran (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <))$
19	0 18	wceq	$wff lim sup = (x \in V ⟼ inf (ran (k \in ℝ ⟼ sup (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <))$

Metamath Proof Explorer

Definition df-limsup

Detailed syntax breakdown