---

Step * 1 of Lemma no-retraction-case-0


1. k : ℕ
2. K : 0-dim-complex
3. 0 < ||K||
4. retraction(|K|;rn-prod-metric(k);{p:ℝ^k| ¬¬(∃c∈[]. in-rat-cube(k;p;c))} )
5. p : |K|
⊢ False
BY
{ (D -2
   THEN (Assert {p:ℝ^k| ¬¬(∃i:ℕ0. in-rat-cube(k;p;⊥))}  BY
               (UseWitness ⌜f p⌝⋅ THEN Auto))
   THEN D -1
   THEN Auto
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  K  :  0-dim-complex
3.  0  <  ||K||
4.  retraction(|K|;rn-prod-metric(k);\{p:\mBbbR{}\^{}k|  \mneg{}\mneg{}(\mexists{}c\mmember{}[].  in-rat-cube(k;p;c))\}  )
5.  p  :  |K|
\mvdash{}  False


By

---

Latex:
(D  -2
  THEN  (Assert  \{p:\mBbbR{}\^{}k|  \mneg{}\mneg{}(\mexists{}i:\mBbbN{}0.  in-rat-cube(k;p;\mbot{}))\}    BY
                          (UseWitness  \mkleeneopen{}f  p\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  D  -1
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index