Definition df-bigo 42342

Description: Define the function "big-O", mapping a real function g to the set of real functions "of order g(x)". Definition in section 1.1 of [AhoHopUll] p. 2. This is a generalisation of "big-O of one", see df-o1 14221 and df-lo1 14222. As explained in the comment of df-o1 , any big-O can be represented in terms of O(1) and division, see elbigolo1 42351. (Contributed by AV, 15-May-2020.)

Assertion

Ref	Expression
df-bigo	|- _O = ( g e. ( RR ^pm RR ) |-> { 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 x. ( g ` y ) ) } )

Distinct variable group:   f, g, x, m, y

Detailed syntax breakdown of Definition df-bigo

Step	Hyp	Ref	Expression
1		cbigo 42341	. 2 class _O
2		vg	. . 3 setvar g
3		cr 9935	. . . 4 class RR
4		cpm 7858	. . . 4 class ^pm
5	3, 3, 4	co 6650	. . 3 class ( RR ^pm RR )
6		vy	. . . . . . . . . 10 setvar y
7	6	cv 1482	. . . . . . . . 9 class y
8		vf	. . . . . . . . . 10 setvar f
9	8	cv 1482	. . . . . . . . 9 class f
10	7, 9	cfv 5888	. . . . . . . 8 class ( f ` y )
11		vm	. . . . . . . . . 10 setvar m
12	11	cv 1482	. . . . . . . . 9 class m
13	2	cv 1482	. . . . . . . . . 10 class g
14	7, 13	cfv 5888	. . . . . . . . 9 class ( g ` y )
15		cmul 9941	. . . . . . . . 9 class x.
16	12, 14, 15	co 6650	. . . . . . . 8 class ( m x. ( g ` y ) )
17		cle 10075	. . . . . . . 8 class <_
18	10, 16, 17	wbr 4653	. . . . . . 7 wff ( f ` y ) <_ ( m x. ( g ` y ) )
19	9	cdm 5114	. . . . . . . 8 class dom f
20		vx	. . . . . . . . . 10 setvar x
21	20	cv 1482	. . . . . . . . 9 class x
22		cpnf 10071	. . . . . . . . 9 class +oo
23		cico 12177	. . . . . . . . 9 class [,)
24	21, 22, 23	co 6650	. . . . . . . 8 class ( x [,) +oo )
25	19, 24	cin 3573	. . . . . . 7 class ( dom f i^i ( x [,) +oo ) )
26	18, 6, 25	wral 2912	. . . . . 6 wff A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) )
27	26, 11, 3	wrex 2913	. . . . 5 wff E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) )
28	27, 20, 3	wrex 2913	. . . 4 wff E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) )
29	28, 8, 5	crab 2916	. . 3 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 x. ( g ` y ) ) }
30	2, 5, 29	cmpt 4729	. 2 class ( g e. ( RR ^pm RR ) |-> { 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 x. ( g ` y ) ) } )
31	1, 30	wceq 1483	1 wff _O = ( g e. ( RR ^pm RR ) |-> { 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 x. ( g ` y ) ) } )

This definition is referenced by:  bigoval  42343  elbigofrcl  42344