---

Step * of Lemma remove-singularity

∀[X:Type]. ∀[d:metric(X)].
  ∀k:ℕ. ∀f:{p:ℝ^k| r0 < ||p||}  ⟶ X. ∀z:X.
    ((∃c:{c:ℝ| r0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (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 < ||p||} . g p ≡ f p))))
BY
{ (InstLemma `remove-singularity-seq-mcauchy` []
   THEN RepeatFor 6 ((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-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. f : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. z : X
6. ∃c:{c:ℝ| r0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
7. cau : ∀[p:ℝ^k]. mcauchy(d;n.remove-singularity-seq(k;p;f;z) n)
8. cmplt : mcomplete(X with d)
9. p : ℝ^k
10. req-vec(k;p;λi.r0)
⊢ lim n→∞.remove-singularity-seq(k;p;f;z) n = z

2
1. X : Type
2. d : metric(X)
3. k : ℕ
4. f : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. z : X
6. ∃c:{c:ℝ| r0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
7. cau : ∀[p:ℝ^k]. mcauchy(d;n.remove-singularity-seq(k;p;f;z) n)
8. cmplt : mcomplete(X with d)
9. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ cauchy-mlimit(cmplt;remove-singularity-seq(k;p;f;z);cau) ≡ z)
10. p : {p:ℝ^k| r0 < ||p||} 
⊢ lim n→∞.remove-singularity-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  <  ||p||\}    {}\mrightarrow{}  X.  \mforall{}z:X.
        ((\mexists{}c:\{c:\mBbbR{}|  r0  \mleq{}  c\} 
              \mforall{}m:\mBbbN{}\msupplus{}.  \mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}  .    ((||p||  \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  <  ||p||\}  .  g  p  \mequiv{}  f  p))))


By

---

Latex:
(InstLemma  `remove-singularity-seq-mcauchy`  []
  THEN  RepeatFor  6  ((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-seq(k;p;f;z);cau)\mkleeneclose{} 
  THEN  Reduce  0
  THEN  Auto
  THEN  BLemma  `cauchy-mlimit-unique`
  THEN  Auto)

---

Home Index