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

Definition df-lo1 15210
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 15206 . 2 class ≤𝑂(1)
2 vy . . . . . . . . 9 setvar 𝑦
32cv 1538 . . . . . . . 8 class 𝑦
4 vf . . . . . . . . 9 setvar 𝑓
54cv 1538 . . . . . . . 8 class 𝑓
63, 5cfv 6426 . . . . . . 7 class (𝑓𝑦)
7 vm . . . . . . . 8 setvar 𝑚
87cv 1538 . . . . . . 7 class 𝑚
9 cle 11020 . . . . . . 7 class
106, 8, 9wbr 5073 . . . . . 6 wff (𝑓𝑦) ≤ 𝑚
115cdm 5584 . . . . . . 7 class dom 𝑓
12 vx . . . . . . . . 9 setvar 𝑥
1312cv 1538 . . . . . . . 8 class 𝑥
14 cpnf 11016 . . . . . . . 8 class +∞
15 cico 13091 . . . . . . . 8 class [,)
1613, 14, 15co 7267 . . . . . . 7 class (𝑥[,)+∞)
1711, 16cin 3885 . . . . . 6 class (dom 𝑓 ∩ (𝑥[,)+∞))
1810, 2, 17wral 3064 . . . . 5 wff 𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚
19 cr 10880 . . . . 5 class
2018, 7, 19wrex 3065 . . . 4 wff 𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚
2120, 12, 19wrex 3065 . . 3 wff 𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚
22 cpm 8603 . . . 4 class pm
2319, 19, 22co 7267 . . 3 class (ℝ ↑pm ℝ)
2421, 4, 23crab 3068 . 2 class {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚}
251, 24wceq 1539 1 wff ≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ 𝑚}
Colors of variables: wff setvar class
This definition is referenced by:  ello1  15234
  Copyright terms: Public domain W3C validator