Metamath Proof Explorer


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 ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )