Definition df-o1 14849

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 14845	. 2 class 𝑂(1)
2		vy	. . . . . . . . . 10 setvar 𝑦
3	2	cv 1536	. . . . . . . . 9 class 𝑦
4		vf	. . . . . . . . . 10 setvar 𝑓
5	4	cv 1536	. . . . . . . . 9 class 𝑓
6	3, 5	cfv 6357	. . . . . . . 8 class (𝑓‘𝑦)
7		cabs 14595	. . . . . . . 8 class abs
8	6, 7	cfv 6357	. . . . . . 7 class (abs‘(𝑓‘𝑦))
9		vm	. . . . . . . 8 setvar 𝑚
10	9	cv 1536	. . . . . . 7 class 𝑚
11		cle 10678	. . . . . . 7 class ≤
12	8, 10, 11	wbr 5068	. . . . . 6 wff (abs‘(𝑓‘𝑦)) ≤ 𝑚
13	5	cdm 5557	. . . . . . 7 class dom 𝑓
14		vx	. . . . . . . . 9 setvar 𝑥
15	14	cv 1536	. . . . . . . 8 class 𝑥
16		cpnf 10674	. . . . . . . 8 class +∞
17		cico 12743	. . . . . . . 8 class [,)
18	15, 16, 17	co 7158	. . . . . . 7 class (𝑥[,)+∞)
19	13, 18	cin 3937	. . . . . 6 class (dom 𝑓 ∩ (𝑥[,)+∞))
20	12, 2, 19	wral 3140	. . . . 5 wff ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
21		cr 10538	. . . . 5 class ℝ
22	20, 9, 21	wrex 3141	. . . 4 wff ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
23	22, 14, 21	wrex 3141	. . 3 wff ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
24		cc 10537	. . . 4 class ℂ
25		cpm 8409	. . . 4 class ↑pm
26	24, 21, 25	co 7158	. . 3 class (ℂ ↑pm ℝ)
27	23, 4, 26	crab 3144	. 2 class {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}
28	1, 27	wceq 1537	1 wff 𝑂(1) = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}

This definition is referenced by:  elo1  14885