---

Step * of Lemma remove-singularity-max

∀[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)))))
    ⇒ mcomplete(X with d)
    ⇒ (∃g:ℝ^k ⟶ X
         ((∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)) ∧ (∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p))))
BY
{ (InstLemma `remove-singularity-max-seq-mcauchy` []
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN (Assert λi.r0 ∈ ℝ^k BY
               Auto)
   THEN PromoteHyp (-1) 4
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN (D 0 THENA Auto)
   THEN RenameVar `cau' (-2)
   THEN RenameVar `cmplt' (-1)
   THEN D 0 With ⌜λp.cauchy-mlimit(cmplt;remove-singularity-max-seq(k;p;f;z);cau)⌝ 
   THEN Reduce 0
   THEN Auto
   THEN BLemma `cauchy-mlimit-unique`
   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)
⊢ lim n→∞.remove-singularity-max-seq(k;p;f;z) n = z

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} 
    ∀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)} 
⊢ lim n→∞.remove-singularity-max-seq(k;p;f;z) n = f p

---

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{}  mcomplete(X  with  d)
        {}\mRightarrow{}  (\mexists{}g:\mBbbR{}\^{}k  {}\mrightarrow{}  X
                  ((\mforall{}p:\mBbbR{}\^{}k.  (req-vec(k;p;\mlambda{}i.r0)  {}\mRightarrow{}  g  p  \mequiv{}  z))
                  \mwedge{}  (\mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}  .  g  p  \mequiv{}  f  p))))


By

---

Latex:
(InstLemma  `remove-singularity-max-seq-mcauchy`  []
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  (Assert  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}k  BY
                          Auto)
  THEN  PromoteHyp  (-1)  4
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  RenameVar  `cau'  (-2)
  THEN  RenameVar  `cmplt'  (-1)
  THEN  D  0  With  \mkleeneopen{}\mlambda{}p.cauchy-mlimit(cmplt;remove-singularity-max-seq(k;p;f;z);cau)\mkleeneclose{} 
  THEN  Reduce  0
  THEN  Auto
  THEN  BLemma  `cauchy-mlimit-unique`
  THEN  Auto)

---

Home Index