---

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

∀[n:ℕ]. ∀[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))} ].
  (g ∈ sphere-map(n))
BY
{ (Auto THEN MemTypeCD THEN Auto) }

1
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))} 
⊢ g ∈ S(n) ⟶ S(n)

2
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))))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[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))\}  ].
    (g  \mmember{}  sphere-map(n))


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto)

---

Home Index