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

Definition df-o1 13541
Description: Define the set of eventually bounded functions. We don't bother to build the full conception of big-O notation, because we can represent any big-O in terms of  O(1) and division, and any little-O in terms of a limit and division. We could also use limsup for this, but it only works on integer sequences, while this will work for real sequences or integer sequences. (Contributed by Mario Carneiro, 15-Sep-2014.)
Assertion
Ref Expression
df-o1  |-  O(1)  =  {
f  e.  ( CC 
^pm  RR )  |  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( abs `  ( f `  y
) )  <_  m }
Distinct variable group:    x, y, f, m

Detailed syntax breakdown of Definition df-o1
StepHypRef Expression
1 co1 13537 . 2  class  O(1)
2 vy . . . . . . . . . 10  setvar  y
32cv 1436 . . . . . . . . 9  class  y
4 vf . . . . . . . . . 10  setvar  f
54cv 1436 . . . . . . . . 9  class  f
63, 5cfv 5597 . . . . . . . 8  class  ( f `
 y )
7 cabs 13285 . . . . . . . 8  class  abs
86, 7cfv 5597 . . . . . . 7  class  ( abs `  ( f `  y
) )
9 vm . . . . . . . 8  setvar  m
109cv 1436 . . . . . . 7  class  m
11 cle 9676 . . . . . . 7  class  <_
128, 10, 11wbr 4420 . . . . . 6  wff  ( abs `  ( f `  y
) )  <_  m
135cdm 4849 . . . . . . 7  class  dom  f
14 vx . . . . . . . . 9  setvar  x
1514cv 1436 . . . . . . . 8  class  x
16 cpnf 9672 . . . . . . . 8  class +oo
17 cico 11637 . . . . . . . 8  class  [,)
1815, 16, 17co 6301 . . . . . . 7  class  ( x [,) +oo )
1913, 18cin 3435 . . . . . 6  class  ( dom  f  i^i  ( x [,) +oo ) )
2012, 2, 19wral 2775 . . . . 5  wff  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( abs `  ( f `  y
) )  <_  m
21 cr 9538 . . . . 5  class  RR
2220, 9, 21wrex 2776 . . . 4  wff  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( abs `  ( f `  y
) )  <_  m
2322, 14, 21wrex 2776 . . 3  wff  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( abs `  ( f `  y
) )  <_  m
24 cc 9537 . . . 4  class  CC
25 cpm 7477 . . . 4  class  ^pm
2624, 21, 25co 6301 . . 3  class  ( CC 
^pm  RR )
2723, 4, 26crab 2779 . 2  class  { f  e.  ( CC  ^pm  RR )  |  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( abs `  ( f `  y
) )  <_  m }
281, 27wceq 1437 1  wff  O(1)  =  {
f  e.  ( CC 
^pm  RR )  |  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,) +oo ) ) ( abs `  ( f `  y
) )  <_  m }
Colors of variables: wff setvar class
This definition is referenced by:  elo1  13577
  Copyright terms: Public domain W3C validator