Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bigo Structured version   Visualization version   GIF version

Definition df-bigo 47234
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 generalization of "big-O of one", see df-o1 15434 and df-lo1 15435. As explained in the comment of df-o1 , any big-O can be represented in terms of ๐‘‚(1) and division, see elbigolo1 47243. (Contributed by AV, 15-May-2020.)
Assertion
Ref Expression
df-bigo ฮŸ = (๐‘” โˆˆ (โ„ โ†‘pm โ„) โ†ฆ {๐‘“ โˆˆ (โ„ โ†‘pm โ„) โˆฃ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘š โˆˆ โ„ โˆ€๐‘ฆ โˆˆ (dom ๐‘“ โˆฉ (๐‘ฅ[,)+โˆž))(๐‘“โ€˜๐‘ฆ) โ‰ค (๐‘š ยท (๐‘”โ€˜๐‘ฆ))})
Distinct variable group:   ๐‘“,๐‘”,๐‘ฅ,๐‘š,๐‘ฆ

Detailed syntax breakdown of Definition df-bigo
StepHypRef Expression
1 cbigo 47233 . 2 class ฮŸ
2 vg . . 3 setvar ๐‘”
3 cr 11109 . . . 4 class โ„
4 cpm 8821 . . . 4 class โ†‘pm
53, 3, 4co 7409 . . 3 class (โ„ โ†‘pm โ„)
6 vy . . . . . . . . . 10 setvar ๐‘ฆ
76cv 1541 . . . . . . . . 9 class ๐‘ฆ
8 vf . . . . . . . . . 10 setvar ๐‘“
98cv 1541 . . . . . . . . 9 class ๐‘“
107, 9cfv 6544 . . . . . . . 8 class (๐‘“โ€˜๐‘ฆ)
11 vm . . . . . . . . . 10 setvar ๐‘š
1211cv 1541 . . . . . . . . 9 class ๐‘š
132cv 1541 . . . . . . . . . 10 class ๐‘”
147, 13cfv 6544 . . . . . . . . 9 class (๐‘”โ€˜๐‘ฆ)
15 cmul 11115 . . . . . . . . 9 class ยท
1612, 14, 15co 7409 . . . . . . . 8 class (๐‘š ยท (๐‘”โ€˜๐‘ฆ))
17 cle 11249 . . . . . . . 8 class โ‰ค
1810, 16, 17wbr 5149 . . . . . . 7 wff (๐‘“โ€˜๐‘ฆ) โ‰ค (๐‘š ยท (๐‘”โ€˜๐‘ฆ))
199cdm 5677 . . . . . . . 8 class dom ๐‘“
20 vx . . . . . . . . . 10 setvar ๐‘ฅ
2120cv 1541 . . . . . . . . 9 class ๐‘ฅ
22 cpnf 11245 . . . . . . . . 9 class +โˆž
23 cico 13326 . . . . . . . . 9 class [,)
2421, 22, 23co 7409 . . . . . . . 8 class (๐‘ฅ[,)+โˆž)
2519, 24cin 3948 . . . . . . 7 class (dom ๐‘“ โˆฉ (๐‘ฅ[,)+โˆž))
2618, 6, 25wral 3062 . . . . . 6 wff โˆ€๐‘ฆ โˆˆ (dom ๐‘“ โˆฉ (๐‘ฅ[,)+โˆž))(๐‘“โ€˜๐‘ฆ) โ‰ค (๐‘š ยท (๐‘”โ€˜๐‘ฆ))
2726, 11, 3wrex 3071 . . . . 5 wff โˆƒ๐‘š โˆˆ โ„ โˆ€๐‘ฆ โˆˆ (dom ๐‘“ โˆฉ (๐‘ฅ[,)+โˆž))(๐‘“โ€˜๐‘ฆ) โ‰ค (๐‘š ยท (๐‘”โ€˜๐‘ฆ))
2827, 20, 3wrex 3071 . . . 4 wff โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘š โˆˆ โ„ โˆ€๐‘ฆ โˆˆ (dom ๐‘“ โˆฉ (๐‘ฅ[,)+โˆž))(๐‘“โ€˜๐‘ฆ) โ‰ค (๐‘š ยท (๐‘”โ€˜๐‘ฆ))
2928, 8, 5crab 3433 . . 3 class {๐‘“ โˆˆ (โ„ โ†‘pm โ„) โˆฃ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘š โˆˆ โ„ โˆ€๐‘ฆ โˆˆ (dom ๐‘“ โˆฉ (๐‘ฅ[,)+โˆž))(๐‘“โ€˜๐‘ฆ) โ‰ค (๐‘š ยท (๐‘”โ€˜๐‘ฆ))}
302, 5, 29cmpt 5232 . 2 class (๐‘” โˆˆ (โ„ โ†‘pm โ„) โ†ฆ {๐‘“ โˆˆ (โ„ โ†‘pm โ„) โˆฃ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘š โˆˆ โ„ โˆ€๐‘ฆ โˆˆ (dom ๐‘“ โˆฉ (๐‘ฅ[,)+โˆž))(๐‘“โ€˜๐‘ฆ) โ‰ค (๐‘š ยท (๐‘”โ€˜๐‘ฆ))})
311, 30wceq 1542 1 wff ฮŸ = (๐‘” โˆˆ (โ„ โ†‘pm โ„) โ†ฆ {๐‘“ โˆˆ (โ„ โ†‘pm โ„) โˆฃ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘š โˆˆ โ„ โˆ€๐‘ฆ โˆˆ (dom ๐‘“ โˆฉ (๐‘ฅ[,)+โˆž))(๐‘“โ€˜๐‘ฆ) โ‰ค (๐‘š ยท (๐‘”โ€˜๐‘ฆ))})
Colors of variables: wff setvar class
This definition is referenced by:  bigoval  47235  elbigofrcl  47236
  Copyright terms: Public domain W3C validator