Metamath Proof Explorer

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 ⊢ O = g ∈ ℝ ↑ 𝑝𝑚 ℝ ⟼ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbigo class O
1 vg setvar g
2 cr class ℝ
3 cpm class ↑ 𝑝𝑚
4 2 2 3 co class ℝ ↑ 𝑝𝑚 ℝ
5 vf setvar f
6 vx setvar x
7 vm setvar m
8 vy setvar y
9 5 cv setvar f
10 9 cdm class dom ⁡ f
11 6 cv setvar x
12 cico class .
13 cpnf class +∞
14 11 13 12 co class x +∞
15 10 14 cin class dom ⁡ f ∩ x +∞
16 8 cv setvar y
17 16 9 cfv class f ⁡ y
18 cle class ≤
19 7 cv setvar m
20 cmul class ×
21 1 cv setvar g
22 16 21 cfv class g ⁡ y
23 19 22 20 co class m ⁢ g ⁡ y
24 17 23 18 wbr wff f ⁡ y ≤ m ⁢ g ⁡ y
25 24 8 15 wral wff ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y
26 25 7 2 wrex wff ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y
27 26 6 2 wrex wff ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y
28 27 5 4 crab class f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y
29 1 4 28 cmpt class g ∈ ℝ ↑ 𝑝𝑚 ℝ ⟼ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y
30 0 29 wceq wff O = g ∈ ℝ ↑ 𝑝𝑚 ℝ ⟼ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y