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

Step	Hyp	Ref	Expression
0		clsi	$class lim inf$
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	cinf	$class inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
15	3 4 14	cmpt	$class (k \in ℝ ⟼ inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
16	15	crn	$class ran (k \in ℝ ⟼ inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
17	16 11 13	csup	$class sup (ran (k \in ℝ ⟼ inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
18	1 2 17	cmpt	$class (x \in V ⟼ sup (ran (k \in ℝ ⟼ inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <))$
19	0 18	wceq	$wff lim inf = (x \in V ⟼ sup (ran (k \in ℝ ⟼ inf (x [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <))$

Metamath Proof Explorer