---

Step * of Lemma remove-singularity-max-mfun

∀[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))
         ∧ (f:FUN({p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} ;X) ⇒ g:FUN(ℝ^k;X)))))
BY
{ (InstLemma `remove-singularity-max` []
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN (Assert λi.r0 ∈ ℝ^k BY
               Auto)
   THEN PromoteHyp (-1) 4
   THEN RepeatFor 5 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN ParallelLast'
   THEN All (RepUR ``so_apply``)
   THEN Auto
   THEN (StableCases ⌜r0 < mdist(max-metric(k);x1;λi.r0)⌝⋅ THENA Auto)
   THEN Try ((FLemma `not-rless` [-1] THENA 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. mcomplete(X with d)
9. g : ℝ^k ⟶ X
10. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
11. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p
12. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
13. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p
14. ∀x1,x2:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .  (x1 ≡ x2 ⇒ f x1 ≡ f x2)
15. x1 : ℝ^k
16. x2 : ℝ^k
17. x1 ≡ x2
18. r0 < mdist(max-metric(k);x1;λi.r0)
⊢ g x1 ≡ g x2

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. mcomplete(X with d)
9. g : ℝ^k ⟶ X
10. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
11. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p
12. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
13. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p
14. ∀x1,x2:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .  (x1 ≡ x2 ⇒ f x1 ≡ f x2)
15. x1 : ℝ^k
16. x2 : ℝ^k
17. x1 ≡ x2
18. ¬(r0 < mdist(max-metric(k);x1;λi.r0))
19. mdist(max-metric(k);x1;λi.r0) ≤ r0
⊢ g x1 ≡ g x2

---

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


By

---

Latex:
(InstLemma  `remove-singularity-max`  []
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  (Assert  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}k  BY
                          Auto)
  THEN  PromoteHyp  (-1)  4
  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  ParallelLast'
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto
  THEN  (StableCases  \mkleeneopen{}r0  <  mdist(max-metric(k);x1;\mlambda{}i.r0)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((FLemma  `not-rless`  [-1]  THENA  Auto)))

---

Home Index