---

Step * of Lemma Degree-implies-BrowerFPT-ext

∀n:ℕ. BrouwerFPT(n + 1) supposing ¬¬DegreeExists(n)
BY
{ Extract of Obid: Degree-implies-BrowerFPT
  not unfolding  find-approx-fp
  finishing with Auto
  normalizes to:
  
  λn,f,e. find-approx-fp(n + 1;f;e) }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  Degree-implies-BrowerFPT
not  unfolding    find-approx-fp
finishing  with  Auto
normalizes  to:

\mlambda{}n,f,e.  find-approx-fp(n  +  1;f;e)

---

Home Index