---

Step * 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
11. req-vec(k;p;λi.r0)
⊢ lim n→∞.remove-singularity-max-seq(k;p;f;z) n = z
BY
{ (Assert ∀n:ℕ. ((remove-singularity-max-seq(k;p;f;z) n) = z ∈ X) BY
         (Auto
          THEN RepUR ``remove-singularity-max-seq`` 0
          THEN AutoSplit
          THEN (Assert r0 < mdist(max-metric(k);p;λi.r0) BY
                      (InstLemma `realvec-max-ibs-property` [⌜k⌝;⌜p⌝]⋅ THEN Auto))
          THEN (Assert mdist(max-metric(k);p;λi.r0) = r0 BY
                      (Unfold `mdist` 0 THEN Fold `meq` 0 THEN EAuto 1))
          THEN Auto)) }

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} 
    ∀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
11. req-vec(k;p;λi.r0)
12. ∀n:ℕ. ((remove-singularity-max-seq(k;p;f;z) n) = z ∈ X)
⊢ lim n→∞.remove-singularity-max-seq(k;p;f;z) n = z

---

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.  p  :  \mBbbR{}\^{}k
11.  req-vec(k;p;\mlambda{}i.r0)
\mvdash{}  lim  n\mrightarrow{}\minfty{}.remove-singularity-max-seq(k;p;f;z)  n  =  z


By

---

Latex:
(Assert  \mforall{}n:\mBbbN{}.  ((remove-singularity-max-seq(k;p;f;z)  n)  =  z)  BY
              (Auto
                THEN  RepUR  ``remove-singularity-max-seq``  0
                THEN  AutoSplit
                THEN  (Assert  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)  BY
                                        (InstLemma  `realvec-max-ibs-property`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto))
                THEN  (Assert  mdist(max-metric(k);p;\mlambda{}i.r0)  =  r0  BY
                                        (Unfold  `mdist`  0  THEN  Fold  `meq`  0  THEN  EAuto  1))
                THEN  Auto))

---

Home Index