---

Step * of Lemma remove-singularity-mfun

∀[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)
         ∧ (f:FUN({p:ℝ^k| r0 < ||p||} ;X) ⇒ g:FUN(ℝ^k;X)))))
BY
{ (InstLemma `remove-singularity` []
   THEN RepeatFor 8 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN ParallelLast'
   THEN All (RepUR ``so_apply``)
   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. mcomplete(X with d)
8. g : ℝ^k ⟶ X
9. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
10. ∀p:{p:ℝ^k| r0 < ||p||} . g p ≡ f p
11. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
12. ∀p:{p:ℝ^k| r0 < ||p||} . g p ≡ f p
13. ∀x1,x2:{p:ℝ^k| r0 < ||p||} .  (x1 ≡ x2 ⇒ f x1 ≡ f x2)
14. x1 : ℝ^k
15. x2 : ℝ^k
16. x1 ≡ x2
⊢ g x1 ≡ g x2

---

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)
                  \mwedge{}  (f:FUN(\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}  ;X)  {}\mRightarrow{}  g:FUN(\mBbbR{}\^{}k;X)))))


By

---

Latex:
(InstLemma  `remove-singularity`  []
  THEN  RepeatFor  8  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  ParallelLast'
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto)

---

Home Index