---

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


1. k : ℕ
2. K : 1-dim-complex
3. 0 < ||K||
4. f : |K| ⟶ |∂(K)|
5. f:FUN(|K|;|∂(K)|)
6. ∀a:|∂(K)|. f a ≡ a
7. ∀c:ℚCube(k). ((c ∈ K) ⇒ (∃x:ℝ^k. ∀p:ℝ^k. ((¬¬in-rat-cube(k;p;c)) ⇒ f p ≡ x)))
⊢ False
BY
{ (Assert ⌜∀s:ℕ. ∀K:1-dim-complex.
             ((||K|| ≤ s)
             ⇒ 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)))⌝⋅
THENM (InstHyp [⌜||K||⌝;⌜K⌝;⌜f⌝] (-1)⋅ THEN Auto)
) }

1
.....assertion..... 
1. k : ℕ
2. K : 1-dim-complex
3. 0 < ||K||
4. f : |K| ⟶ |∂(K)|
5. f:FUN(|K|;|∂(K)|)
6. ∀a:|∂(K)|. f a ≡ a
7. ∀c:ℚCube(k). ((c ∈ K) ⇒ (∃x:ℝ^k. ∀p:ℝ^k. ((¬¬in-rat-cube(k;p;c)) ⇒ f p ≡ x)))
⊢ ∀s:ℕ. ∀K:1-dim-complex.
    ((||K|| ≤ s)
    ⇒ 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)))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  K  :  1-dim-complex
3.  0  <  ||K||
4.  f  :  |K|  {}\mrightarrow{}  |\mpartial{}(K)|
5.  f:FUN(|K|;|\mpartial{}(K)|)
6.  \mforall{}a:|\mpartial{}(K)|.  f  a  \mequiv{}  a
7.  \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)))
\mvdash{}  False


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}s:\mBbbN{}.  \mforall{}K:1-dim-complex.
                      ((||K||  \mleq{}  s)
                      {}\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)))\mkleeneclose{}\mcdot{}
THENM  (InstHyp  [\mkleeneopen{}||K||\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
)

---

Home Index