---

Step * 2 of Lemma sphere-map-from-ball-map


1. n : ℕ
2. g : {g:B(n + 1) ⟶ B(n + 1)| 
        (∀x,y:B(n + 1).  (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))) ∧ (∀x:B(n + 1). (||g x|| = r1))} 
3. k : ℕ+
⊢ ∃d:ℕ+. ∀p,q:S(n).  ((d(p;q) ≤ (r1/r(d))) ⇒ (d(g p;g q) ≤ (r1/r(k))))
BY
{ ((InstLemma `real-ball-uniform-continuity` [⌜n + 1⌝;⌜n + 1⌝;⌜g⌝;⌜(r1/r(k))⌝]⋅ THENA Auto)
   THEN RepeatFor 3 (ParallelLast)
   ) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  g  :  \{g:B(n  +  1)  {}\mrightarrow{}  B(n  +  1)| 
                (\mforall{}x,y:B(n  +  1).    (req-vec(n  +  1;x;y)  {}\mRightarrow{}  req-vec(n  +  1;g  x;g  y)))
                \mwedge{}  (\mforall{}x:B(n  +  1).  (||g  x||  =  r1))\} 
3.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  \mexists{}d:\mBbbN{}\msupplus{}.  \mforall{}p,q:S(n).    ((d(p;q)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(g  p;g  q)  \mleq{}  (r1/r(k))))


By

---

Latex:
((InstLemma  `real-ball-uniform-continuity`  [\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}(r1/r(k))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast)
  )

---

Home Index