Definition df-bigo 49767

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

Assertion

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

Distinct variable group:   𝑓,𝑔,𝑥,𝑚,𝑦

Detailed syntax breakdown of Definition df-bigo

Step	Hyp	Ref	Expression
1		cbigo 49766	. 2 class Ο
2		vg	. . 3 setvar 𝑔
3		cr 11204	. . . 4 class ℝ
4		cpm 8853	. . . 4 class ↑pm
5	3, 3, 4	co 7422	. . 3 class (ℝ ↑pm ℝ)
6		vy	. . . . . . . . . 10 setvar 𝑦
7	6	cv 1568	. . . . . . . . 9 class 𝑦
8		vf	. . . . . . . . . 10 setvar 𝑓
9	8	cv 1568	. . . . . . . . 9 class 𝑓
10	7, 9	cfv 6541	. . . . . . . 8 class (𝑓‘𝑦)
11		vm	. . . . . . . . . 10 setvar 𝑚
12	11	cv 1568	. . . . . . . . 9 class 𝑚
13	2	cv 1568	. . . . . . . . . 10 class 𝑔
14	7, 13	cfv 6541	. . . . . . . . 9 class (𝑔‘𝑦)
15		cmul 11210	. . . . . . . . 9 class ·
16	12, 14, 15	co 7422	. . . . . . . 8 class (𝑚 · (𝑔‘𝑦))
17		cle 11349	. . . . . . . 8 class ≤
18	10, 16, 17	wbr 5102	. . . . . . 7 wff (𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))
19	9	cdm 5650	. . . . . . . 8 class dom 𝑓
20		vx	. . . . . . . . . 10 setvar 𝑥
21	20	cv 1568	. . . . . . . . 9 class 𝑥
22		cpnf 11345	. . . . . . . . 9 class +∞
23		cico 13483	. . . . . . . . 9 class [,)
24	21, 22, 23	co 7422	. . . . . . . 8 class (𝑥[,)+∞)
25	19, 24	cin 4088	. . . . . . 7 class (dom 𝑓 ∩ (𝑥[,)+∞))
26	18, 6, 25	wral 3076	. . . . . 6 wff ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))
27	26, 11, 3	wrex 3086	. . . . 5 wff ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))
28	27, 20, 3	wrex 3086	. . . 4 wff ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))
29	28, 8, 5	crab 3412	. . 3 class {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))}
30	2, 5, 29	cmpt 5185	. 2 class (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))})
31	1, 30	wceq 1569	1 wff Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))})

This definition is used by:  bigoval  49768  elbigofrcl  49769