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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clsi	⊢ lim inf
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	cinf	⊢ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < )
15	3 4 14	cmpt	⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
16	15	crn	⊢ ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
17	16 11 13	csup	⊢ sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < )
18	1 2 17	cmpt	⊢ ( 𝑥 ∈ V ↦ sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
19	0 18	wceq	⊢ lim inf = ( 𝑥 ∈ V ↦ sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )