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 \in (ℝ ↑_{𝑝𝑚} ℝ) ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq 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 \cap [x, +∞))$
16	8	cv	$setvar y$
17	16 9	cfv	$class f (y)$
18		cle	$class \leq$
19	7	cv	$setvar m$
20		cmul	$class \times$
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) \leq m g (y)$
25	24 8 15	wral	$wff \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)$
26	25 7 2	wrex	$wff \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)$
27	26 6 2	wrex	$wff \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)$
28	27 5 4	crab	$class \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)\}$
29	1 4 28	cmpt	$class (g \in (ℝ ↑_{𝑝𝑚} ℝ) ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)\})$
30	0 29	wceq	$wff O = (g \in (ℝ ↑_{𝑝𝑚} ℝ) ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)\})$

Metamath Proof Explorer

Definition df-bigo

Detailed syntax breakdown