Metamath Proof Explorer

Definition df-lo1

Description: Define the set of eventually upper bounded real functions. This fills a gap in O(1) coverage, to express statements like f ( x ) <_ g ( x ) + O ( x ) via ( x e. RR+ |-> ( f ( x ) - g ( x ) ) / x ) e. <_O(1) . (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Assertion df-lo1 ⊢ ≤𝑂⁡1 = f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m

Detailed syntax breakdown

Step Hyp Ref Expression
0 clo1 class ≤𝑂⁡1
1 vf setvar f
2 cr class ℝ
3 cpm class ↑ 𝑝𝑚
4 2 2 3 co class ℝ ↑ 𝑝𝑚 ℝ
5 vx setvar x
6 vm setvar m
7 vy setvar y
8 1 cv setvar f
9 8 cdm class dom ⁡ f
10 5 cv setvar x
11 cico class .
12 cpnf class +∞
13 10 12 11 co class x +∞
14 9 13 cin class dom ⁡ f ∩ x +∞
15 7 cv setvar y
16 15 8 cfv class f ⁡ y
17 cle class ≤
18 6 cv setvar m
19 16 18 17 wbr wff f ⁡ y ≤ m
20 19 7 14 wral wff ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m
21 20 6 2 wrex wff ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m
22 21 5 2 wrex wff ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m
23 22 1 4 crab class f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m
24 0 23 wceq wff ≤𝑂⁡1 = f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m