---

Step * 1 2 1 2 1 1 of Lemma no-retraction-case-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)))
BY
{ (All Thin
   THEN InductionOnNat
   THEN Auto
   THEN (Assert ∀p:ℝ^k. ∀c:ℚCube(k).  ((c ∈ K) ⇒ (¬¬in-rat-cube(k;p;c)) ⇒ (p ∈ |K|)) BY
               (Auto
                THEN MemTypeCD
                THEN Auto
                THEN RepeatFor 2 (ParallelLast)
                THEN RepeatFor 2 (D -2)
                THEN D 0 With ⌜i⌝ 
                THEN Auto))
   THEN (Assert ∀p:ℝ^k. ∀c:ℚCube(k).  ((c ∈ ∂(K)) ⇒ (¬¬in-rat-cube(k;p;c)) ⇒ (p ∈ |∂(K)|)) BY
               ((GenConclTerm ⌜∂(K)⌝⋅ THENA Auto)
                THEN Auto
                THEN MemTypeCD
                THEN Auto
                THEN RepeatFor 2 (ParallelLast)
                THEN RepeatFor 2 (D -2)
                THEN D 0 With ⌜i⌝ 
                THEN Auto))) }

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). ((c ∈ K) ⇒ (∃x:ℝ^k. ∀p:ℝ^k. ((¬¬in-rat-cube(k;p;c)) ⇒ f p ≡ x)))
12. ∀p:ℝ^k. ∀c:ℚCube(k).  ((c ∈ K) ⇒ (¬¬in-rat-cube(k;p;c)) ⇒ (p ∈ |K|))
13. ∀p:ℝ^k. ∀c:ℚCube(k).  ((c ∈ ∂(K)) ⇒ (¬¬in-rat-cube(k;p;c)) ⇒ (p ∈ |∂(K)|))
⊢ False

2
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|

---

Latex:

---

Latex:
.....assertion..... 
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{}  \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)))


By

---

Latex:
(All  Thin
  THEN  InductionOnNat
  THEN  Auto
  THEN  (Assert  \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|))  BY
                          (Auto
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  RepeatFor  2  (ParallelLast)
                            THEN  RepeatFor  2  (D  -2)
                            THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{} 
                            THEN  Auto))
  THEN  (Assert  \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)|))  BY
                          ((GenConclTerm  \mkleeneopen{}\mpartial{}(K)\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  Auto
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  RepeatFor  2  (ParallelLast)
                            THEN  RepeatFor  2  (D  -2)
                            THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{} 
                            THEN  Auto)))

---

Home Index