Definition df-bigo 42140

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 14069 and df-lo1 14070. As explained in the comment of df-o1 , any big-O can be represented in terms of 𝑂(1) and division, see elbigolo1 42149. (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 42139	. 2 class Ο
2		vg	. . 3 setvar 𝑔
3		cr 9814	. . . 4 class ℝ
4		cpm 7745	. . . 4 class ↑pm
5	3, 3, 4	co 6549	. . 3 class (ℝ ↑pm ℝ)
6		vy	. . . . . . . . . 10 setvar 𝑦
7	6	cv 1474	. . . . . . . . 9 class 𝑦
8		vf	. . . . . . . . . 10 setvar 𝑓
9	8	cv 1474	. . . . . . . . 9 class 𝑓
10	7, 9	cfv 5804	. . . . . . . 8 class (𝑓‘𝑦)
11		vm	. . . . . . . . . 10 setvar 𝑚
12	11	cv 1474	. . . . . . . . 9 class 𝑚
13	2	cv 1474	. . . . . . . . . 10 class 𝑔
14	7, 13	cfv 5804	. . . . . . . . 9 class (𝑔‘𝑦)
15		cmul 9820	. . . . . . . . 9 class ·
16	12, 14, 15	co 6549	. . . . . . . 8 class (𝑚 · (𝑔‘𝑦))
17		cle 9954	. . . . . . . 8 class ≤
18	10, 16, 17	wbr 4583	. . . . . . 7 wff (𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))
19	9	cdm 5038	. . . . . . . 8 class dom 𝑓
20		vx	. . . . . . . . . 10 setvar 𝑥
21	20	cv 1474	. . . . . . . . 9 class 𝑥
22		cpnf 9950	. . . . . . . . 9 class +∞
23		cico 12048	. . . . . . . . 9 class [,)
24	21, 22, 23	co 6549	. . . . . . . 8 class (𝑥[,)+∞)
25	19, 24	cin 3539	. . . . . . 7 class (dom 𝑓 ∩ (𝑥[,)+∞))
26	18, 6, 25	wral 2896	. . . . . 6 wff ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))
27	26, 11, 3	wrex 2897	. . . . 5 wff ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))
28	27, 20, 3	wrex 2897	. . . 4 wff ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))
29	28, 8, 5	crab 2900	. . 3 class {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))}
30	2, 5, 29	cmpt 4643	. 2 class (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))})
31	1, 30	wceq 1475	1 wff Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))})

This definition is referenced by:  bigoval  42141  elbigofrcl  42142