Definition df-o1 15637

Description: Define the set of eventually bounded functions. We don't bother to build the full conception of big-O notation, because we can represent any big-O in terms of 𝑂(1) and division, and any little-O in terms of a limit and division. We could also use limsup for this, but it only works on integer sequences, while this will work for real sequences or integer sequences. (Contributed by Mario Carneiro, 15-Sep-2014.)

Assertion

Ref	Expression
df-o1	⊢ 𝑂(1) = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}

Distinct variable group:   𝑥,𝑦,𝑓,𝑚

Detailed syntax breakdown of Definition df-o1

Step	Hyp	Ref	Expression
1		co1 15633	. 2 class 𝑂(1)
2		vy	. . . . . . . . . 10 setvar 𝑦
3	2	cv 1569	. . . . . . . . 9 class 𝑦
4		vf	. . . . . . . . . 10 setvar 𝑓
5	4	cv 1569	. . . . . . . . 9 class 𝑓
6	3, 5	cfv 6531	. . . . . . . 8 class (𝑓‘𝑦)
7		cabs 15381	. . . . . . . 8 class abs
8	6, 7	cfv 6531	. . . . . . 7 class (abs‘(𝑓‘𝑦))
9		vm	. . . . . . . 8 setvar 𝑚
10	9	cv 1569	. . . . . . 7 class 𝑚
11		cle 11325	. . . . . . 7 class ≤
12	8, 10, 11	wbr 5103	. . . . . 6 wff (abs‘(𝑓‘𝑦)) ≤ 𝑚
13	5	cdm 5651	. . . . . . 7 class dom 𝑓
14		vx	. . . . . . . . 9 setvar 𝑥
15	14	cv 1569	. . . . . . . 8 class 𝑥
16		cpnf 11321	. . . . . . . 8 class +∞
17		cico 13459	. . . . . . . 8 class [,)
18	15, 16, 17	co 7412	. . . . . . 7 class (𝑥[,)+∞)
19	13, 18	cin 3898	. . . . . 6 class (dom 𝑓 ∩ (𝑥[,)+∞))
20	12, 2, 19	wral 3077	. . . . 5 wff ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
21		cr 11180	. . . . 5 class ℝ
22	20, 9, 21	wrex 3087	. . . 4 wff ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
23	22, 14, 21	wrex 3087	. . 3 wff ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
24		cc 11179	. . . 4 class ℂ
25		cpm 8832	. . . 4 class ↑pm
26	24, 21, 25	co 7412	. . 3 class (ℂ ↑pm ℝ)
27	23, 4, 26	crab 3413	. 2 class {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}
28	1, 27	wceq 1570	1 wff 𝑂(1) = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}

This definition is used by:  elo1  15673