---

Step * of Lemma NoBallRetraction-implies-BrouwerFPT

∀n:ℕ. BrouwerFPT(n) supposing NoBallRetraction(n)
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN InstLemma `approx-fixpoint-unit-ball-2` [⌜n⌝;⌜f⌝;⌜e⌝]⋅
   THEN Auto
   THEN Thin (-1)
   THEN D -1
   THEN MemTypeCD
   THEN (Auto THEN Thin (-1))
   THEN (D 0 THENA Auto)) }

1
1. n : ℕ
2. NoBallRetraction(n)
3. f : B(n) ⟶ B(n)
4. ∀x,y:B(n).  (req-vec(n;x;y) ⇒ req-vec(n;f x;f y))
5. ∀x:B(n). f x ≠ x
⊢ False

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  BrouwerFPT(n)  supposing  NoBallRetraction(n)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  InstLemma  `approx-fixpoint-unit-ball-2`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  (Auto  THEN  Thin  (-1))
  THEN  (D  0  THENA  Auto))

---

Home Index