Definition df-o1 15662

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 15658	. 2 class 𝑂(1)
2		vy	. . . . . . . . . 10 setvar 𝑦
3	2	cv 1568	. . . . . . . . 9 class 𝑦
4		vf	. . . . . . . . . 10 setvar 𝑓
5	4	cv 1568	. . . . . . . . 9 class 𝑓
6	3, 5	cfv 6538	. . . . . . . 8 class (𝑓‘𝑦)
7		cabs 15406	. . . . . . . 8 class abs
8	6, 7	cfv 6538	. . . . . . 7 class (abs‘(𝑓‘𝑦))
9		vm	. . . . . . . 8 setvar 𝑚
10	9	cv 1568	. . . . . . 7 class 𝑚
11		cle 11347	. . . . . . 7 class ≤
12	8, 10, 11	wbr 5102	. . . . . 6 wff (abs‘(𝑓‘𝑦)) ≤ 𝑚
13	5	cdm 5650	. . . . . . 7 class dom 𝑓
14		vx	. . . . . . . . 9 setvar 𝑥
15	14	cv 1568	. . . . . . . 8 class 𝑥
16		cpnf 11343	. . . . . . . 8 class +∞
17		cico 13481	. . . . . . . 8 class [,)
18	15, 16, 17	co 7420	. . . . . . 7 class (𝑥[,)+∞)
19	13, 18	cin 4089	. . . . . 6 class (dom 𝑓 ∩ (𝑥[,)+∞))
20	12, 2, 19	wral 3076	. . . . 5 wff ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
21		cr 11202	. . . . 5 class ℝ
22	20, 9, 21	wrex 3086	. . . 4 wff ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
23	22, 14, 21	wrex 3086	. . 3 wff ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
24		cc 11201	. . . 4 class ℂ
25		cpm 8851	. . . 4 class ↑pm
26	24, 21, 25	co 7420	. . 3 class (ℂ ↑pm ℝ)
27	23, 4, 26	crab 3412	. 2 class {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}
28	1, 27	wceq 1569	1 wff 𝑂(1) = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}

This definition is used by:  elo1  15698