df-lo1

Description: Define the set of eventually upper bounded real functions. This fills a gap in O(1) coverage, to express statements like f ( x ) <_ g ( x ) + O ( x ) via ( x e. RR+ |-> ( f ( x ) - g ( x ) ) / x ) e. <_O(1) . (Contributed by Mario Carneiro, 25-May-2016)

		Ref	Expression
	Assertion	df-lo1	$⊢ \leq 𝑂 (1) = \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clo1	$class \leq 𝑂 (1)$
1		vf	$setvar f$
2		cr	$class ℝ$
3		cpm	$class ↑_{𝑝𝑚}$
4	2 2 3	co	$class (ℝ ↑_{𝑝𝑚} ℝ)$
5		vx	$setvar x$
6		vm	$setvar m$
7		vy	$setvar y$
8	1	cv	$setvar f$
9	8	cdm	$class dom f$
10	5	cv	$setvar x$
11		cico	$class [.)$
12		cpnf	$class +∞$
13	10 12 11	co	$class [x, +∞)$
14	9 13	cin	$class (dom f \cap [x, +∞))$
15	7	cv	$setvar y$
16	15 8	cfv	$class f (y)$
17		cle	$class \leq$
18	6	cv	$setvar m$
19	16 18 17	wbr	$wff f (y) \leq m$
20	19 7 14	wral	$wff \forall y \in (dom f \cap [x, +∞)) f (y) \leq m$
21	20 6 2	wrex	$wff \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m$
22	21 5 2	wrex	$wff \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m$
23	22 1 4	crab	$class \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m\}$
24	0 23	wceq	$wff \leq 𝑂 (1) = \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m\}$

Metamath Proof Explorer

Definition df-lo1

Detailed syntax breakdown