Definition df-o1 15394

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 15390	. 2 class 𝑂(1)
2		vy	. . . . . . . . . 10 setvar 𝑦
3	2	cv 1540	. . . . . . . . 9 class 𝑦
4		vf	. . . . . . . . . 10 setvar 𝑓
5	4	cv 1540	. . . . . . . . 9 class 𝑓
6	3, 5	cfv 6481	. . . . . . . 8 class (𝑓‘𝑦)
7		cabs 15138	. . . . . . . 8 class abs
8	6, 7	cfv 6481	. . . . . . 7 class (abs‘(𝑓‘𝑦))
9		vm	. . . . . . . 8 setvar 𝑚
10	9	cv 1540	. . . . . . 7 class 𝑚
11		cle 11144	. . . . . . 7 class ≤
12	8, 10, 11	wbr 5091	. . . . . 6 wff (abs‘(𝑓‘𝑦)) ≤ 𝑚
13	5	cdm 5616	. . . . . . 7 class dom 𝑓
14		vx	. . . . . . . . 9 setvar 𝑥
15	14	cv 1540	. . . . . . . 8 class 𝑥
16		cpnf 11140	. . . . . . . 8 class +∞
17		cico 13244	. . . . . . . 8 class [,)
18	15, 16, 17	co 7346	. . . . . . 7 class (𝑥[,)+∞)
19	13, 18	cin 3901	. . . . . 6 class (dom 𝑓 ∩ (𝑥[,)+∞))
20	12, 2, 19	wral 3047	. . . . 5 wff ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
21		cr 11002	. . . . 5 class ℝ
22	20, 9, 21	wrex 3056	. . . 4 wff ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
23	22, 14, 21	wrex 3056	. . 3 wff ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
24		cc 11001	. . . 4 class ℂ
25		cpm 8751	. . . 4 class ↑pm
26	24, 21, 25	co 7346	. . 3 class (ℂ ↑pm ℝ)
27	23, 4, 26	crab 3395	. 2 class {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}
28	1, 27	wceq 1541	1 wff 𝑂(1) = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}

This definition is referenced by:  elo1  15430