This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Detailed syntax breakdown

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