MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-limsup Structured version   Visualization version   GIF version

Definition df-limsup 13996
Description: Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 13999 for its value. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 11-Sep-2020.)
Assertion
Ref Expression
df-limsup lim sup = (𝑥 ∈ V ↦ inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
Distinct variable group:   𝑥,𝑘

Detailed syntax breakdown of Definition df-limsup
StepHypRef Expression
1 clsp 13995 . 2 class lim sup
2 vx . . 3 setvar 𝑥
3 cvv 3172 . . 3 class V
4 vk . . . . . 6 setvar 𝑘
5 cr 9791 . . . . . 6 class
62cv 1473 . . . . . . . . 9 class 𝑥
74cv 1473 . . . . . . . . . 10 class 𝑘
8 cpnf 9927 . . . . . . . . . 10 class +∞
9 cico 12004 . . . . . . . . . 10 class [,)
107, 8, 9co 6527 . . . . . . . . 9 class (𝑘[,)+∞)
116, 10cima 5031 . . . . . . . 8 class (𝑥 “ (𝑘[,)+∞))
12 cxr 9929 . . . . . . . 8 class *
1311, 12cin 3538 . . . . . . 7 class ((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*)
14 clt 9930 . . . . . . 7 class <
1513, 12, 14csup 8206 . . . . . 6 class sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )
164, 5, 15cmpt 4637 . . . . 5 class (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
1716crn 5029 . . . 4 class ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
1817, 12, 14cinf 8207 . . 3 class inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < )
192, 3, 18cmpt 4637 . 2 class (𝑥 ∈ V ↦ inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
201, 19wceq 1474 1 wff lim sup = (𝑥 ∈ V ↦ inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
Colors of variables: wff setvar class
This definition is referenced by:  limsupcl  13998  limsupval  13999
  Copyright terms: Public domain W3C validator