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

Definition df-lo1 12981
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 12977 . 2  class  <_O(1)
2 vy . . . . . . . . 9  setvar  y
32cv 1368 . . . . . . . 8  class  y
4 vf . . . . . . . . 9  setvar  f
54cv 1368 . . . . . . . 8  class  f
63, 5cfv 5430 . . . . . . 7  class  ( f `
 y )
7 vm . . . . . . . 8  setvar  m
87cv 1368 . . . . . . 7  class  m
9 cle 9431 . . . . . . 7  class  <_
106, 8, 9wbr 4304 . . . . . 6  wff  ( f `
 y )  <_  m
115cdm 4852 . . . . . . 7  class  dom  f
12 vx . . . . . . . . 9  setvar  x
1312cv 1368 . . . . . . . 8  class  x
14 cpnf 9427 . . . . . . . 8  class +oo
15 cico 11314 . . . . . . . 8  class  [,)
1613, 14, 15co 6103 . . . . . . 7  class  ( x [,) +oo )
1711, 16cin 3339 . . . . . 6  class  ( dom  f  i^i  ( x [,) +oo ) )
1810, 2, 17wral 2727 . . . . 5  wff  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( f `
 y )  <_  m
19 cr 9293 . . . . 5  class  RR
2018, 7, 19wrex 2728 . . . 4  wff  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( f `
 y )  <_  m
2120, 12, 19wrex 2728 . . 3  wff  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( f `
 y )  <_  m
22 cpm 7227 . . . 4  class  ^pm
2319, 19, 22co 6103 . . 3  class  ( RR 
^pm  RR )
2421, 4, 23crab 2731 . 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 1369 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  13005
  Copyright terms: Public domain W3C validator