---

Step * 2 of Lemma unit-cube-to-unit-ball


1. n : ℕ+
2. max-metric(n) ≤ rn-metric(n)
3. rn-metric(n) ≤ r(n)*max-metric(n)
4. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
⊢ ∃g:ℝ^n ⟶ ℝ^n
   ((∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0))
   ∧ (∀p:{p:ℝ^n| r0 < ||p||} . g p ≡ (λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p) p)
   ∧ (g ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}  ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} )
   ∧ g:FUN(ℝ^n;ℝ^n))
BY
{ (((Assert ∀p:{p:ℝ^n| r0 < ||p||} . ((mdist(max-metric(n);λi.r0;p)/||p||)*p ∈ ℝ^n) BY
           ((D 0 THENA Auto) THEN D -1 THEN RepeatFor 2 (MemCD) THEN Try (OrRight) THEN Auto))
    THEN (Assert λi.r0 ∈ ℝ^n BY
                Auto)
    )
   THEN (InstLemma `remove-singularity-mfun` [⌜ℝ^n⌝;⌜max-metric(n)⌝;⌜n⌝;⌜λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p⌝;
         ⌜λi.r0⌝]⋅
         THENA (Auto THEN Reduce 0 THEN D 0 With ⌜r(4)⌝  THEN Auto)
         )
   ) }

1
1. n : ℕ+
2. max-metric(n) ≤ rn-metric(n)
3. rn-metric(n) ≤ r(n)*max-metric(n)
4. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
5. ∀p:{p:ℝ^n| r0 < ||p||} . ((mdist(max-metric(n);λi.r0;p)/||p||)*p ∈ ℝ^n)
6. λi.r0 ∈ ℝ^n
7. m : ℕ+
8. p : {p:ℝ^n| r0 < ||p||} 
9. ||p|| ≤ (r(4)/r(m))
⊢ mdist(max-metric(n);(mdist(max-metric(n);λi.r0;p)/||p||)*p;λi.r0) ≤ (r(4)/r(m))

2
1. n : ℕ+
2. max-metric(n) ≤ rn-metric(n)
3. rn-metric(n) ≤ r(n)*max-metric(n)
4. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
5. ∀p:{p:ℝ^n| r0 < ||p||} . ((mdist(max-metric(n);λi.r0;p)/||p||)*p ∈ ℝ^n)
6. λi.r0 ∈ ℝ^n
7. ∃g:ℝ^n ⟶ ℝ^n
    ((∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0))
    ∧ (∀p:{p:ℝ^n| r0 < ||p||} . g p ≡ (λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p) p)
    ∧ (λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p:FUN({p:ℝ^n| r0 < ||p||} ;ℝ^n) ⇒ g:FUN(ℝ^n;ℝ^n)))
⊢ ∃g:ℝ^n ⟶ ℝ^n
   ((∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0))
   ∧ (∀p:{p:ℝ^n| r0 < ||p||} . g p ≡ (λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p) p)
   ∧ (g ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}  ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} )
   ∧ g:FUN(ℝ^n;ℝ^n))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  max-metric(n)  \mleq{}  rn-metric(n)
3.  rn-metric(n)  \mleq{}  r(n)*max-metric(n)
4.  \mforall{}p:\mBbbR{}\^{}n.  (r0  <  ||p||  \mLeftarrow{}{}\mRightarrow{}  r0  <  mdist(max-metric(n);\mlambda{}i.r0;p))
\mvdash{}  \mexists{}g:\mBbbR{}\^{}n  {}\mrightarrow{}  \mBbbR{}\^{}n
      ((\mforall{}p:\mBbbR{}\^{}n.  (req-vec(n;p;\mlambda{}i.r0)  {}\mRightarrow{}  g  p  \mequiv{}  \mlambda{}i.r0))
      \mwedge{}  (\mforall{}p:\{p:\mBbbR{}\^{}n|  r0  <  ||p||\}  .  g  p  \mequiv{}  (\mlambda{}p.(mdist(max-metric(n);\mlambda{}i.r0;p)/||p||)*p)  p)
      \mwedge{}  (g  \mmember{}  \{q:\mBbbR{}\^{}n|  mdist(max-metric(n);\mlambda{}i.r0;q)  \mleq{}  r1\}    {}\mrightarrow{}  \{q:\mBbbR{}\^{}n|  mdist(rn-metric(n);\mlambda{}i.r0;q)  \mleq{}  r1\}  )
      \mwedge{}  g:FUN(\mBbbR{}\^{}n;\mBbbR{}\^{}n))


By

---

Latex:
(((Assert  \mforall{}p:\{p:\mBbbR{}\^{}n|  r0  <  ||p||\}  .  ((mdist(max-metric(n);\mlambda{}i.r0;p)/||p||)*p  \mmember{}  \mBbbR{}\^{}n)  BY
                  ((D  0  THENA  Auto)  THEN  D  -1  THEN  RepeatFor  2  (MemCD)  THEN  Try  (OrRight)  THEN  Auto))
    THEN  (Assert  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}n  BY
                            Auto)
    )
  THEN  (InstLemma  `remove-singularity-mfun`  [\mkleeneopen{}\mBbbR{}\^{}n\mkleeneclose{};\mkleeneopen{}max-metric(n)\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};
              \mkleeneopen{}\mlambda{}p.(mdist(max-metric(n);\mlambda{}i.r0;p)/||p||)*p\mkleeneclose{};\mkleeneopen{}\mlambda{}i.r0\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Reduce  0  THEN  D  0  With  \mkleeneopen{}r(4)\mkleeneclose{}    THEN  Auto)
              )
  )

---

Home Index