---

Step * 1 2 1 2 1 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)|))
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
BY
{ ((Assert dim(c) = 1 ∈ ℤ BY
          ((DVar `K' THEN Auto) THEN RWO "l_all_iff" 8 THEN Auto))
   THEN (RWO "-1" (-3) THENA Auto)
   THEN Reduce -3) }

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) = 0 ∈ ℤ
21. ↑in-complex-boundary(k;b;K)
22. dim(c) = 1 ∈ ℤ
⊢ 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)|))
14.  b  :  \mBbbQ{}Cube(k)
15.  (b  \mmember{}  \mpartial{}(K))
16.  c  :  \mBbbQ{}Cube(k)
17.  (c  \mmember{}  K)
18.  \muparrow{}Inhabited(c)
19.  b  \mleq{}  c
20.  dim(b)  =  (dim(c)  -  1)
21.  \muparrow{}in-complex-boundary(k;b;K)
\mvdash{}  False


By

---

Latex:
((Assert  dim(c)  =  1  BY
                ((DVar  `K'  THEN  Auto)  THEN  RWO  "l\_all\_iff"  8  THEN  Auto))
  THEN  (RWO  "-1"  (-3)  THENA  Auto)
  THEN  Reduce  -3)

---

Home Index