---

Step * 2 1 of Lemma remove-singularity-max


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} 
    ∀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))))
8. cau : ∀[p:ℝ^k]. mcauchy(d;n.remove-singularity-max-seq(k;p;f;z) n)
9. cmplt : mcomplete(X with d)
10. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ cauchy-mlimit(cmplt;remove-singularity-max-seq(k;p;f;z);cau) ≡ z)
11. p : {p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} 
12. r0 < mdist(max-metric(k);p;λi.r0)
13. (r0 < mdist(max-metric(k);p;λi.r0)) ⇐ ∃n:ℕ. ((realvec-max-ibs(k;p) n) = 1 ∈ ℤ)
14. ∀n:ℕ. (((realvec-max-ibs(k;p) n) = 0 ∈ ℤ) ⇒ (mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(n + 1))))
15. n : ℕ
16. (realvec-max-ibs(k;p) n) = 1 ∈ ℤ
17. ∀[n@0:ℕ]. (realvec-max-ibs(k;p) n@0) = 1 ∈ ℤ supposing n ≤ n@0
18. k@0 : ℕ+
19. n@0 : ℕ
20. n ≤ n@0
⊢ mdist(d;remove-singularity-max-seq(k;p;f;z) n@0;f p) ≤ (r1/r(k@0))
BY
{ (RepUR ``remove-singularity-max-seq`` 0
   THEN (RWO "-4" 0 THENA Auto)
   THEN Reduce 0
   THEN RWO "mdist-same" 0
   THEN Auto) }

---

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.  \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))))
8.  cau  :  \mforall{}[p:\mBbbR{}\^{}k].  mcauchy(d;n.remove-singularity-max-seq(k;p;f;z)  n)
9.  cmplt  :  mcomplete(X  with  d)
10.  \mforall{}p:\mBbbR{}\^{}k.  (req-vec(k;p;\mlambda{}i.r0)  {}\mRightarrow{}  cauchy-mlimit(cmplt;remove-singularity-max-seq(k;p;f;z);cau)  \mequiv{}  z)
11.  p  :  \{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\} 
12.  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)
13.  (r0  <  mdist(max-metric(k);p;\mlambda{}i.r0))  \mLeftarrow{}{}  \mexists{}n:\mBbbN{}.  ((realvec-max-ibs(k;p)  n)  =  1)
14.  \mforall{}n:\mBbbN{}.  (((realvec-max-ibs(k;p)  n)  =  0)  {}\mRightarrow{}  (mdist(max-metric(k);p;\mlambda{}i.r0)  \mleq{}  (r(4)/r(n  +  1))))
15.  n  :  \mBbbN{}
16.  (realvec-max-ibs(k;p)  n)  =  1
17.  \mforall{}[n@0:\mBbbN{}].  (realvec-max-ibs(k;p)  n@0)  =  1  supposing  n  \mleq{}  n@0
18.  k@0  :  \mBbbN{}\msupplus{}
19.  n@0  :  \mBbbN{}
20.  n  \mleq{}  n@0
\mvdash{}  mdist(d;remove-singularity-max-seq(k;p;f;z)  n@0;f  p)  \mleq{}  (r1/r(k@0))


By

---

Latex:
(RepUR  ``remove-singularity-max-seq``  0
  THEN  (RWO  "-4"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RWO  "mdist-same"  0
  THEN  Auto)

---

Home Index