---

Step * 1 of Lemma Degree-implies-BrowerFPT


1. n : ℕ
2. ind : sphere-map(n) ⟶ ℤ
3. ∀f,g:sphere-map(n).  (sphere-map-eq(n;f;g) ⇒ ((ind f) = (ind g) ∈ ℤ))
4. ∀p:S(n). ((ind const-sphere-map(p)) = 0 ∈ ℤ)
5. (ind id-sphere-map()) = 1 ∈ ℤ
6. g : B(n + 1) ⟶ B(n + 1)
7. ∀x,y:B(n + 1).  (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))
8. ∀x:B(n + 1). (||g x|| = r1)
9. ∀x:B(n + 1). ((||x|| = r1) ⇒ req-vec(n + 1;g x;x))
⊢ False
BY
{ (Assert ∀h:{h:B(n + 1) ⟶ B(n + 1)| ∀p,q:B(n + 1).  (req-vec(n + 1;p;q) ⇒ req-vec(n + 1;h p;h q))} 
            (g o h ∈ sphere-map(n)) BY
         (Intro
          THEN BLemma `sphere-map-from-ball-map`
          THEN Try (Trivial)
          THEN MemTypeCD
          THEN Reduce 0
          THEN Auto
          THEN BackThruSomeHyp
          THEN DVar `h'
          THEN Unhide
          THEN Auto
          THEN RepUR ``req-vec`` 0
          THEN Auto)) }

1
1. n : ℕ
2. ind : sphere-map(n) ⟶ ℤ
3. ∀f,g:sphere-map(n).  (sphere-map-eq(n;f;g) ⇒ ((ind f) = (ind g) ∈ ℤ))
4. ∀p:S(n). ((ind const-sphere-map(p)) = 0 ∈ ℤ)
5. (ind id-sphere-map()) = 1 ∈ ℤ
6. g : B(n + 1) ⟶ B(n + 1)
7. ∀x,y:B(n + 1).  (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))
8. ∀x:B(n + 1). (||g x|| = r1)
9. ∀x:B(n + 1). ((||x|| = r1) ⇒ req-vec(n + 1;g x;x))
10. ∀h:{h:B(n + 1) ⟶ B(n + 1)| ∀p,q:B(n + 1).  (req-vec(n + 1;p;q) ⇒ req-vec(n + 1;h p;h q))} . (g o h ∈ sphere-map(n)\000C)
⊢ False

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  ind  :  sphere-map(n)  {}\mrightarrow{}  \mBbbZ{}
3.  \mforall{}f,g:sphere-map(n).    (sphere-map-eq(n;f;g)  {}\mRightarrow{}  ((ind  f)  =  (ind  g)))
4.  \mforall{}p:S(n).  ((ind  const-sphere-map(p))  =  0)
5.  (ind  id-sphere-map())  =  1
6.  g  :  B(n  +  1)  {}\mrightarrow{}  B(n  +  1)
7.  \mforall{}x,y:B(n  +  1).    (req-vec(n  +  1;x;y)  {}\mRightarrow{}  req-vec(n  +  1;g  x;g  y))
8.  \mforall{}x:B(n  +  1).  (||g  x||  =  r1)
9.  \mforall{}x:B(n  +  1).  ((||x||  =  r1)  {}\mRightarrow{}  req-vec(n  +  1;g  x;x))
\mvdash{}  False


By

---

Latex:
(Assert  \mforall{}h:\{h:B(n  +  1)  {}\mrightarrow{}  B(n  +  1)|  \mforall{}p,q:B(n  +  1).    (req-vec(n  +  1;p;q)  {}\mRightarrow{}  req-vec(n  +  1;h  p;h  q))\} 
                    (g  o  h  \mmember{}  sphere-map(n))  BY
              (Intro
                THEN  BLemma  `sphere-map-from-ball-map`
                THEN  Try  (Trivial)
                THEN  MemTypeCD
                THEN  Reduce  0
                THEN  Auto
                THEN  BackThruSomeHyp
                THEN  DVar  `h'
                THEN  Unhide
                THEN  Auto
                THEN  RepUR  ``req-vec``  0
                THEN  Auto))

---

Home Index