---

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

∀[X:Type]. ∀[d:metric(X)]. ∀[k:ℕ]. ∀[f:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X]. ∀[z:X].
  ((∃c:{c:ℝ| r0 ≤ c} 
     ∀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)))))
  ⇒ (∀[p:ℝ^k]. mcauchy(d;n.remove-singularity-max-seq(k;p;f;z) n)))
BY
{ (RepeatFor 3 (Intro)
   THEN (Assert λi.r0 ∈ ℝ^k BY
               Auto)
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN ExRepD
   THEN RenameVar `b' (-1)) }

1
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)))))]

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[k:\mBbbN{}].  \mforall{}[f:\{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}    {}\mrightarrow{}  X].  \mforall{}[z:X].
    ((\mexists{}c:\{c:\mBbbR{}|  r0  \mleq{}  c\} 
          \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)))))
    {}\mRightarrow{}  (\mforall{}[p:\mBbbR{}\^{}k].  mcauchy(d;n.remove-singularity-max-seq(k;p;f;z)  n)))


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (Assert  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}k  BY
                          Auto)
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `b'  (-1))

---

Home Index