Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lo1 Structured version   Visualization version   GIF version

Definition df-lo1 14441
 Description: Define the set of eventually upper bounded real functions. This fills a gap in 𝑂(1) coverage, to express statements like 𝑓(𝑥) ≤ 𝑔(𝑥) + 𝑂(𝑥) via (𝑥 ∈ ℝ+ ↦ (𝑓(𝑥) − 𝑔(𝑥)) / 𝑥) ∈ ≤𝑂(1). (Contributed by Mario Carneiro, 25-May-2016.)
Assertion
Ref Expression
df-lo1 ≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚}
Distinct variable group:   𝑥,𝑦,𝑓,𝑚

Detailed syntax breakdown of Definition df-lo1
StepHypRef Expression
1 clo1 14437 . 2 class ≤𝑂(1)
2 vy . . . . . . . . 9 setvar 𝑦
32cv 1631 . . . . . . . 8 class 𝑦
4 vf . . . . . . . . 9 setvar 𝑓
54cv 1631 . . . . . . . 8 class 𝑓
63, 5cfv 6049 . . . . . . 7 class (𝑓𝑦)
7 vm . . . . . . . 8 setvar 𝑚
87cv 1631 . . . . . . 7 class 𝑚
9 cle 10287 . . . . . . 7 class
106, 8, 9wbr 4804 . . . . . 6 wff (𝑓𝑦) ≤ 𝑚
115cdm 5266 . . . . . . 7 class dom 𝑓
12 vx . . . . . . . . 9 setvar 𝑥
1312cv 1631 . . . . . . . 8 class 𝑥
14 cpnf 10283 . . . . . . . 8 class +∞
15 cico 12390 . . . . . . . 8 class [,)
1613, 14, 15co 6814 . . . . . . 7 class (𝑥[,)+∞)
1711, 16cin 3714 . . . . . 6 class (dom 𝑓 ∩ (𝑥[,)+∞))
1810, 2, 17wral 3050 . . . . 5 wff 𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚
19 cr 10147 . . . . 5 class
2018, 7, 19wrex 3051 . . . 4 wff 𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚
2120, 12, 19wrex 3051 . . 3 wff 𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚
22 cpm 8026 . . . 4 class pm
2319, 19, 22co 6814 . . 3 class (ℝ ↑pm ℝ)
2421, 4, 23crab 3054 . 2 class {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚}
251, 24wceq 1632 1 wff ≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚}
 Colors of variables: wff setvar class This definition is referenced by:  ello1  14465
 Copyright terms: Public domain W3C validator