---

Step * 1 1 1 of Lemma remove-singularity-seq-mcauchy


1. [X] : Type
2. [d] : metric(X)
3. [k] : ℕ
4. [f] : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. [z] : X
6. c : {c:ℝ| r0 ≤ c} 
7. ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
8. [p] : ℝ^k
9. b : ℕ+
10. n : ℕ
11. (r(-n) ≤ c) ∧ (c ≤ r(n))
⊢ ∃N:ℕ+. ((c/r(N)) ≤ (r1/r(b)))
BY
{ CaseNat 0 `n' }

1
1. [X] : Type
2. [d] : metric(X)
3. [k] : ℕ
4. [f] : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. [z] : X
6. c : {c:ℝ| r0 ≤ c} 
7. ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
8. [p] : ℝ^k
9. b : ℕ+
10. n : ℕ
11. (r(-n) ≤ c) ∧ (c ≤ r(n))
12. n = 0 ∈ ℤ
⊢ ∃N:ℕ+. ((c/r(N)) ≤ (r1/r(b)))

2
1. [X] : Type
2. [d] : metric(X)
3. [k] : ℕ
4. [f] : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. [z] : X
6. c : {c:ℝ| r0 ≤ c} 
7. ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
8. [p] : ℝ^k
9. b : ℕ+
10. n : ℕ
11. (r(-n) ≤ c) ∧ (c ≤ r(n))
12. ¬(n = 0 ∈ ℤ)
⊢ ∃N:ℕ+. ((c/r(N)) ≤ (r1/r(b)))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  [d]  :  metric(X)
3.  [k]  :  \mBbbN{}
4.  [f]  :  \{p:\mBbbR{}\^{}k|  r0  <  ||p||\}    {}\mrightarrow{}  X
5.  [z]  :  X
6.  c  :  \{c:\mBbbR{}|  r0  \mleq{}  c\} 
7.  \mforall{}m:\mBbbN{}\msupplus{}.  \mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}  .    ((||p||  \mleq{}  (r(4)/r(m)))  {}\mRightarrow{}  (mdist(d;f  p;z)  \mleq{}  (c/r(m))))
8.  [p]  :  \mBbbR{}\^{}k
9.  b  :  \mBbbN{}\msupplus{}
10.  n  :  \mBbbN{}
11.  (r(-n)  \mleq{}  c)  \mwedge{}  (c  \mleq{}  r(n))
\mvdash{}  \mexists{}N:\mBbbN{}\msupplus{}.  ((c/r(N))  \mleq{}  (r1/r(b)))


By

---

Latex:
CaseNat  0  `n'

---

Home Index