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

Definition df-limsup 12266
 Description: Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 12269 for its value. (Contributed by NM, 26-Oct-2005.)
Assertion
Ref Expression
df-limsup
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-limsup
StepHypRef Expression
1 clsp 12265 . 2
2 vx . . 3
3 cvv 2957 . . 3
4 vk . . . . . 6
5 cr 8990 . . . . . 6
62cv 1652 . . . . . . . . 9
74cv 1652 . . . . . . . . . 10
8 cpnf 9118 . . . . . . . . . 10
9 cico 10919 . . . . . . . . . 10
107, 8, 9co 6082 . . . . . . . . 9
116, 10cima 4882 . . . . . . . 8
12 cxr 9120 . . . . . . . 8
1311, 12cin 3320 . . . . . . 7
14 clt 9121 . . . . . . 7
1513, 12, 14csup 7446 . . . . . 6
164, 5, 15cmpt 4267 . . . . 5
1716crn 4880 . . . 4
1814ccnv 4878 . . . 4
1917, 12, 18csup 7446 . . 3
202, 3, 19cmpt 4267 . 2
211, 20wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  limsupcl  12268  limsupval  12269
 Copyright terms: Public domain W3C validator