# 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$