---

Step * of Lemma Degree-implies-BrowerFPT

∀n:ℕ. BrouwerFPT(n + 1) supposing ¬¬DegreeExists(n)
BY
{ (Auto
   THEN (InstLemma `NoBallRetraction-implies-BrouwerFPT` [⌜n + 1⌝]⋅ THEN Auto)
   THEN (D 0 THENA Auto)
   THEN (SupposeMore 2 THENA Auto)
   THEN D 2
   THEN ExRepD) }

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))
⊢ False

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  BrouwerFPT(n  +  1)  supposing  \mneg{}\mneg{}DegreeExists(n)


By

---

Latex:
(Auto
  THEN  (InstLemma  `NoBallRetraction-implies-BrouwerFPT`  [\mkleeneopen{}n  +  1\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (SupposeMore  2  THENA  Auto)
  THEN  D  2
  THEN  ExRepD)

---

Home Index