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

Definition df-lo1 11967
Description: Define the set of eventually upper bounded real functions. This fills a gap in  O ( 1 ) coverage, to express statements like  f (
x )  <_  g
( x )  +  O ( x ) via  ( x  e.  RR+  |->  ( f ( x )  -  g
( x ) )  /  x )  e. 
<_ O ( 1 ). (Contributed by Mario Carneiro, 25-May-2016.)
Assertion
Ref Expression
df-lo1  |-  <_ O
( 1 )  =  { f  e.  ( RR  ^pm  RR )  |  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) 
+oo ) ) ( f `  y )  <_  m }
Distinct variable group:    x, y, f, m

Detailed syntax breakdown of Definition df-lo1
StepHypRef Expression
1 clo1 11963 . 2  class  <_ O
( 1 )
2 vy . . . . . . . . 9  set  y
32cv 1624 . . . . . . . 8  class  y
4 vf . . . . . . . . 9  set  f
54cv 1624 . . . . . . . 8  class  f
63, 5cfv 5257 . . . . . . 7  class  ( f `
 y )
7 vm . . . . . . . 8  set  m
87cv 1624 . . . . . . 7  class  m
9 cle 8870 . . . . . . 7  class  <_
106, 8, 9wbr 4025 . . . . . 6  wff  ( f `
 y )  <_  m
115cdm 4691 . . . . . . 7  class  dom  f
12 vx . . . . . . . . 9  set  x
1312cv 1624 . . . . . . . 8  class  x
14 cpnf 8866 . . . . . . . 8  class  +oo
15 cico 10660 . . . . . . . 8  class  [,)
1613, 14, 15co 5860 . . . . . . 7  class  ( x [,)  +oo )
1711, 16cin 3153 . . . . . 6  class  ( dom  f  i^i  ( x [,)  +oo ) )
1810, 2, 17wral 2545 . . . . 5  wff  A. y  e.  ( dom  f  i^i  ( x [,)  +oo ) ) ( f `
 y )  <_  m
19 cr 8738 . . . . 5  class  RR
2018, 7, 19wrex 2546 . . . 4  wff  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,)  +oo ) ) ( f `
 y )  <_  m
2120, 12, 19wrex 2546 . . 3  wff  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,)  +oo ) ) ( f `
 y )  <_  m
22 cpm 6775 . . . 4  class  ^pm
2319, 19, 22co 5860 . . 3  class  ( RR 
^pm  RR )
2421, 4, 23crab 2549 . 2  class  { f  e.  ( RR  ^pm  RR )  |  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,)  +oo ) ) ( f `
 y )  <_  m }
251, 24wceq 1625 1  wff  <_ O
( 1 )  =  { f  e.  ( RR  ^pm  RR )  |  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) 
+oo ) ) ( f `  y )  <_  m }
Colors of variables: wff set class
This definition is referenced by:  ello1  11991
  Copyright terms: Public domain W3C validator