---

Step * 1 1 of Lemma derivative-rinv-basic


1. m : {m:ℕ+| icompact(i-approx((r0, ∞);m))} @i
⊢ ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx((r0, ∞);m)) ⇒ (c ≤ |x|))))]
BY
{ All (RepUR ``i-approx``)⋅ }

1
1. m : {m:ℕ+| icompact([r0 + (r1/r(m)), r(m)])} @i
⊢ ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((((r0 + (r1/r(m))) ≤ x) ∧ (x ≤ r(m))) ⇒ (c ≤ |x|))))]

---

Latex:

---

Latex:

1.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx((r0,  \minfty{});m))\}  @i
\mvdash{}  \mexists{}c:\mBbbR{}  [((r0  <  c)  \mwedge{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx((r0,  \minfty{});m))  {}\mRightarrow{}  (c  \mleq{}  |x|))))]


By

---

Latex:
All  (RepUR  ``i-approx``)\mcdot{}

---

Home Index