Definition df-bigo

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 and df-lo1 . As explained in the comment of df-o1 , any big-O can be represented in terms of O(1) and division, see elbigolo1 . (Contributed by AV, 15-May-2020)

	Ref	Expression
Assertion	df-bigo	⊢ Ο = ( 𝑔 ∈ ( ℝ ↑pm ℝ ) ↦ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbigo	⊢ Ο
1		vg	⊢ 𝑔
2		cr	⊢ ℝ
3		cpm	⊢ ↑pm
4	2 2 3	co	⊢ ( ℝ ↑pm ℝ )
5		vf	⊢ 𝑓
6		vx	⊢ 𝑥
7		vm	⊢ 𝑚
8		vy	⊢ 𝑦
9	5	cv	⊢ 𝑓
10	9	cdm	⊢ dom 𝑓
11	6	cv	⊢ 𝑥
12		cico	⊢ [,)
13		cpnf	⊢ +∞
14	11 13 12	co	⊢ ( 𝑥 [,) +∞ )
15	10 14	cin	⊢ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) )
16	8	cv	⊢ 𝑦
17	16 9	cfv	⊢ ( 𝑓 ‘ 𝑦 )
18		cle	⊢ ≤
19	7	cv	⊢ 𝑚
20		cmul	⊢ ·
21	1	cv	⊢ 𝑔
22	16 21	cfv	⊢ ( 𝑔 ‘ 𝑦 )
23	19 22 20	co	⊢ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) )
24	17 23 18	wbr	⊢ ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) )
25	24 8 15	wral	⊢ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) )
26	25 7 2	wrex	⊢ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) )
27	26 6 2	wrex	⊢ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) )
28	27 5 4	crab	⊢ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) }
29	1 4 28	cmpt	⊢ ( 𝑔 ∈ ( ℝ ↑pm ℝ ) ↦ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } )
30	0 29	wceq	⊢ Ο = ( 𝑔 ∈ ( ℝ ↑pm ℝ ) ↦ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } )