Metamath Proof Explorer

Definition df-lo1

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)

Ref Expression
Assertion 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 }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clo1 
 |-  <_O(1)
1 vf 
 |-  f
2 cr 
 |-  RR
3 cpm 
 |-  ^pm
4 2 2 3 co 
 |-  ( RR ^pm RR )
5 vx 
 |-  x
6 vm 
 |-  m
7 vy 
 |-  y
8 1 cv 
 |-  f
9 8 cdm 
 |-  dom f
10 5 cv 
 |-  x
11 cico 
 |-  [,)
12 cpnf 
 |-  +oo
13 10 12 11 co 
 |-  ( x [,) +oo )
14 9 13 cin 
 |-  ( dom f i^i ( x [,) +oo ) )
15 7 cv 
 |-  y
16 15 8 cfv 
 |-  ( f ` y )
17 cle 
 |-  <_
18 6 cv 
 |-  m
19 16 18 17 wbr 
 |-  ( f ` y ) <_ m
20 19 7 14 wral 
 |-  A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m
21 20 6 2 wrex 
 |-  E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m
22 21 5 2 wrex 
 |-  E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m
23 22 1 4 crab 
 |-  { 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 }
24 0 23 wceq 
 |-  <_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 }