Definition df-o1 15440

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 15436	. 2 class 𝑂(1)
2		vy	. . . . . . . . . 10 setvar 𝑦
3	2	cv 1538	. . . . . . . . 9 class 𝑦
4		vf	. . . . . . . . . 10 setvar 𝑓
5	4	cv 1538	. . . . . . . . 9 class 𝑓
6	3, 5	cfv 6544	. . . . . . . 8 class (𝑓‘𝑦)
7		cabs 15187	. . . . . . . 8 class abs
8	6, 7	cfv 6544	. . . . . . 7 class (abs‘(𝑓‘𝑦))
9		vm	. . . . . . . 8 setvar 𝑚
10	9	cv 1538	. . . . . . 7 class 𝑚
11		cle 11255	. . . . . . 7 class ≤
12	8, 10, 11	wbr 5149	. . . . . 6 wff (abs‘(𝑓‘𝑦)) ≤ 𝑚
13	5	cdm 5677	. . . . . . 7 class dom 𝑓
14		vx	. . . . . . . . 9 setvar 𝑥
15	14	cv 1538	. . . . . . . 8 class 𝑥
16		cpnf 11251	. . . . . . . 8 class +∞
17		cico 13332	. . . . . . . 8 class [,)
18	15, 16, 17	co 7413	. . . . . . 7 class (𝑥[,)+∞)
19	13, 18	cin 3948	. . . . . 6 class (dom 𝑓 ∩ (𝑥[,)+∞))
20	12, 2, 19	wral 3059	. . . . 5 wff ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
21		cr 11113	. . . . 5 class ℝ
22	20, 9, 21	wrex 3068	. . . 4 wff ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
23	22, 14, 21	wrex 3068	. . 3 wff ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚
24		cc 11112	. . . 4 class ℂ
25		cpm 8825	. . . 4 class ↑pm
26	24, 21, 25	co 7413	. . 3 class (ℂ ↑pm ℝ)
27	23, 4, 26	crab 3430	. 2 class {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}
28	1, 27	wceq 1539	1 wff 𝑂(1) = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚}

This definition is referenced by:  elo1  15476