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

Definition df-lo1 13396
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 13392 . 2  class  <_O(1)
2 vy . . . . . . . . 9  setvar  y
32cv 1397 . . . . . . . 8  class  y
4 vf . . . . . . . . 9  setvar  f
54cv 1397 . . . . . . . 8  class  f
63, 5cfv 5570 . . . . . . 7  class  ( f `
 y )
7 vm . . . . . . . 8  setvar  m
87cv 1397 . . . . . . 7  class  m
9 cle 9618 . . . . . . 7  class  <_
106, 8, 9wbr 4439 . . . . . 6  wff  ( f `
 y )  <_  m
115cdm 4988 . . . . . . 7  class  dom  f
12 vx . . . . . . . . 9  setvar  x
1312cv 1397 . . . . . . . 8  class  x
14 cpnf 9614 . . . . . . . 8  class +oo
15 cico 11534 . . . . . . . 8  class  [,)
1613, 14, 15co 6270 . . . . . . 7  class  ( x [,) +oo )
1711, 16cin 3460 . . . . . 6  class  ( dom  f  i^i  ( x [,) +oo ) )
1810, 2, 17wral 2804 . . . . 5  wff  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( f `
 y )  <_  m
19 cr 9480 . . . . 5  class  RR
2018, 7, 19wrex 2805 . . . 4  wff  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( f `
 y )  <_  m
2120, 12, 19wrex 2805 . . 3  wff  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( f `
 y )  <_  m
22 cpm 7413 . . . 4  class  ^pm
2319, 19, 22co 6270 . . 3  class  ( RR 
^pm  RR )
2421, 4, 23crab 2808 . 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 1398 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 setvar class
This definition is referenced by:  ello1  13420
  Copyright terms: Public domain W3C validator