---

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


1. k : ℕ
2. s : ℤ
3. 0 < s
4. ∀K:1-dim-complex
     ((||K|| ≤ (s - 1))
     ⇒ 0 < ||K||
     ⇒ (∀f:|K| ⟶ |∂(K)|
           (f:FUN(|K|;|∂(K)|)
           ⇒ (∀a:|∂(K)|. f a ≡ a)
           ⇒ (∀c:ℚCube(k). ((c ∈ K) ⇒ (∃x:ℝ^k. ∀p:ℝ^k. ((¬¬in-rat-cube(k;p;c)) ⇒ f p ≡ x))))
           ⇒ False)))
5. K : 1-dim-complex
6. ||K|| ≤ s
7. 0 < ||K||
8. f : |K| ⟶ |∂(K)|
9. f:FUN(|K|;|∂(K)|)
10. ∀a:|∂(K)|. f a ≡ a
11. c : ℚCube(k)
12. x : (c ∈ K)
13. x1 : ℝ^k
14. p : ℝ^k
15. x2 : ¬¬in-rat-cube(k;p;c)
16. ∀p:ℝ^k. ∀c:ℚCube(k).  ((c ∈ K) ⇒ (¬¬in-rat-cube(k;p;c)) ⇒ (p ∈ |K|))
17. ∀p:ℝ^k. ∀c:ℚCube(k).  ((c ∈ ∂(K)) ⇒ (¬¬in-rat-cube(k;p;c)) ⇒ (p ∈ |∂(K)|))
⊢ p ∈ |K|
BY
{ (InstHyp [⌜p⌝;⌜c⌝] (-2)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  s  :  \mBbbZ{}
3.  0  <  s
4.  \mforall{}K:1-dim-complex
          ((||K||  \mleq{}  (s  -  1))
          {}\mRightarrow{}  0  <  ||K||
          {}\mRightarrow{}  (\mforall{}f:|K|  {}\mrightarrow{}  |\mpartial{}(K)|
                      (f:FUN(|K|;|\mpartial{}(K)|)
                      {}\mRightarrow{}  (\mforall{}a:|\mpartial{}(K)|.  f  a  \mequiv{}  a)
                      {}\mRightarrow{}  (\mforall{}c:\mBbbQ{}Cube(k).  ((c  \mmember{}  K)  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}\^{}k.  \mforall{}p:\mBbbR{}\^{}k.  ((\mneg{}\mneg{}in-rat-cube(k;p;c))  {}\mRightarrow{}  f  p  \mequiv{}  x))))
                      {}\mRightarrow{}  False)))
5.  K  :  1-dim-complex
6.  ||K||  \mleq{}  s
7.  0  <  ||K||
8.  f  :  |K|  {}\mrightarrow{}  |\mpartial{}(K)|
9.  f:FUN(|K|;|\mpartial{}(K)|)
10.  \mforall{}a:|\mpartial{}(K)|.  f  a  \mequiv{}  a
11.  c  :  \mBbbQ{}Cube(k)
12.  x  :  (c  \mmember{}  K)
13.  x1  :  \mBbbR{}\^{}k
14.  p  :  \mBbbR{}\^{}k
15.  x2  :  \mneg{}\mneg{}in-rat-cube(k;p;c)
16.  \mforall{}p:\mBbbR{}\^{}k.  \mforall{}c:\mBbbQ{}Cube(k).    ((c  \mmember{}  K)  {}\mRightarrow{}  (\mneg{}\mneg{}in-rat-cube(k;p;c))  {}\mRightarrow{}  (p  \mmember{}  |K|))
17.  \mforall{}p:\mBbbR{}\^{}k.  \mforall{}c:\mBbbQ{}Cube(k).    ((c  \mmember{}  \mpartial{}(K))  {}\mRightarrow{}  (\mneg{}\mneg{}in-rat-cube(k;p;c))  {}\mRightarrow{}  (p  \mmember{}  |\mpartial{}(K)|))
\mvdash{}  p  \mmember{}  |K|


By

---

Latex:
(InstHyp  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)

---

Home Index