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

Definition df-o1 13126
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 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
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-o1
StepHypRef Expression
1 co1 13122 . 2
2 vy . . . . . . . . . 10
32cv 1369 . . . . . . . . 9
4 vf . . . . . . . . . 10
54cv 1369 . . . . . . . . 9
63, 5cfv 5537 . . . . . . . 8
7 cabs 12881 . . . . . . . 8
86, 7cfv 5537 . . . . . . 7
9 vm . . . . . . . 8
109cv 1369 . . . . . . 7
11 cle 9556 . . . . . . 7
128, 10, 11wbr 4409 . . . . . 6
135cdm 4957 . . . . . . 7
14 vx . . . . . . . . 9
1514cv 1369 . . . . . . . 8
16 cpnf 9552 . . . . . . . 8
17 cico 11441 . . . . . . . 8
1815, 16, 17co 6222 . . . . . . 7
1913, 18cin 3441 . . . . . 6
2012, 2, 19wral 2800 . . . . 5
21 cr 9418 . . . . 5
2220, 9, 21wrex 2801 . . . 4
2322, 14, 21wrex 2801 . . 3
24 cc 9417 . . . 4
25 cpm 7349 . . . 4
2624, 21, 25co 6222 . . 3
2723, 4, 26crab 2804 . 2
281, 27wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  elo1  13162
  Copyright terms: Public domain W3C validator