---

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


1. [X] : Type
2. [d] : metric(X)
3. [k] : ℕ
4. λi.r0 ∈ ℝ^k
5. [f] : {p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X
6. [z] : X
7. c : {c:ℝ| r0 ≤ c} 
8. ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .
     ((mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
9. [p] : ℝ^k
10. b : ℕ+
⊢ ∃N:ℕ [(∀n,m:ℕ.
           ((N ≤ n)
           ⇒ (N ≤ m)
           ⇒ (mdist(d;remove-singularity-max-seq(k;p;f;z) n;remove-singularity-max-seq(k;p;f;z) m) ≤ (r1/r(b)))))]
BY
{ Assert ⌜∃N:ℕ+. ((c/r(N)) ≤ (r1/r(b)))⌝⋅ }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}N:\mBbbN{}\msupplus{}.  ((c/r(N))  \mleq{}  (r1/r(b)))\mkleeneclose{}\mcdot{}

---

Home Index