---

Step * 1 2 1 2 1 1 1 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). ((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
BY
{ ((Assert ∃b:ℚCube(k). (b ∈ ∂(K)) BY
          ((Assert |∂(K)| BY
                  ((FLemma `rat-cube-complex-polyhedron-inhabited` [7] THENA Auto)
                   THEN RenameVar `p' (-1)
                   THEN UseWitness ⌜f p⌝⋅
                   THEN Auto))
           THEN MoveToConcl (-1)
           THEN (GenConclTerm ⌜∂(K)⌝⋅ THENA Auto)
           THEN (D 0 THENA Auto)
           THEN RepeatFor 2 (DVar `v')
           THEN ((D 0 With ⌜u⌝  THEN Auto)
           ORELSE ((Assert ⌜False⌝⋅ THEN Auto) THEN D -1 THEN Reduce -1 THEN Auto THEN D -1 THEN Auto)
           )))
   THEN D -1
   THEN DupHyp (-1)
   THEN (RWO "member-rat-complex-boundary" (-1) THENA Auto)
   THEN ExRepD) }

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)|))
14. b : ℚCube(k)
15. (b ∈ ∂(K))
16. c : ℚCube(k)
17. (c ∈ K)
18. ↑Inhabited(c)
19. b ≤ c
20. dim(b) = (dim(c) - 1) ∈ ℤ
21. ↑in-complex-boundary(k;b;K)
⊢ False

---

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.  \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)))
12.  \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|))
13.  \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{}  False


By

---

Latex:
((Assert  \mexists{}b:\mBbbQ{}Cube(k).  (b  \mmember{}  \mpartial{}(K))  BY
                ((Assert  |\mpartial{}(K)|  BY
                                ((FLemma  `rat-cube-complex-polyhedron-inhabited`  [7]  THENA  Auto)
                                  THEN  RenameVar  `p'  (-1)
                                  THEN  UseWitness  \mkleeneopen{}f  p\mkleeneclose{}\mcdot{}
                                  THEN  Auto))
                  THEN  MoveToConcl  (-1)
                  THEN  (GenConclTerm  \mkleeneopen{}\mpartial{}(K)\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  (D  0  THENA  Auto)
                  THEN  RepeatFor  2  (DVar  `v')
                  THEN  ((D  0  With  \mkleeneopen{}u\mkleeneclose{}    THEN  Auto)
                  ORELSE  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  D  -1  THEN  Reduce  -1  THEN  Auto  THEN  D  -1  THEN  Auto)
                  )))
  THEN  D  -1
  THEN  DupHyp  (-1)
  THEN  (RWO  "member-rat-complex-boundary"  (-1)  THENA  Auto)
  THEN  ExRepD)

---

Home Index