---

Step * 1 2 1 1 1 1 1 1 1 1 1 1 1 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. ∀x:|∂(K)|. ∃i:ℕ||∂(K)||. req-vec(k;x;λj.rat2real(fst((∂(K)[i] j))))
8. g : x:|∂(K)| ⟶ ℕ||∂(K)||
9. ∀x:|∂(K)|. req-vec(k;x;λj.rat2real(fst((∂(K)[g x] j))))
10. ∀x,y:|∂(K)|.  (x ≡ y ⇒ ((g x) = (g y) ∈ ℤ))
11. ∀x,y:|K|.  (x ≡ y ⇒ ((g (f x)) = (g (f y)) ∈ ℤ))
12. c : ℚCube(k)
13. (c ∈ K)
14. i : ℕk
15. fst((c i)) < snd((c i))
16. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((fst((c j))) = (snd((c j))) ∈ ℚ))
17. ∀x:{x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} 
      (λj.if (j =z i) then x else rat2real(fst((c j))) fi  ∈ |K|)
18. ∀x,y:{x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} .
      ((g (f (λj.if (j =z i) then x else rat2real(fst((c j))) fi )))
      = (g (f (λj.if (j =z i) then y else rat2real(fst((c j))) fi )))
      ∈ ℤ)
19. rat2real(fst((c i))) ∈ {x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} 
20. λj.if (j =z i) then rat2real(fst((c i))) else rat2real(fst((c j))) fi  ∈ |K|
21. ∀p:ℝ^k. ((¬¬in-rat-cube(k;p;c)) ⇒ (p ∈ |K|))
22. p : ℝ^k
23. ¬¬in-rat-cube(k;p;c)
24. x : |K|
25. y : |K|
26. (g (f x)) = (g (f y)) ∈ ℤ
⊢ f x ≡ f y
BY
{ ((Assert req-vec(k;f x;λj.rat2real(fst((∂(K)[g (f x)] j)))) BY
          Auto)
   THEN (Assert req-vec(k;f y;λj.rat2real(fst((∂(K)[g (f y)] j)))) BY
               Auto)
   THEN HypSubst' (-3) (-2)) }

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. ∀x:|∂(K)|. ∃i:ℕ||∂(K)||. req-vec(k;x;λj.rat2real(fst((∂(K)[i] j))))
8. g : x:|∂(K)| ⟶ ℕ||∂(K)||
9. ∀x:|∂(K)|. req-vec(k;x;λj.rat2real(fst((∂(K)[g x] j))))
10. ∀x,y:|∂(K)|.  (x ≡ y ⇒ ((g x) = (g y) ∈ ℤ))
11. ∀x,y:|K|.  (x ≡ y ⇒ ((g (f x)) = (g (f y)) ∈ ℤ))
12. c : ℚCube(k)
13. (c ∈ K)
14. i : ℕk
15. fst((c i)) < snd((c i))
16. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((fst((c j))) = (snd((c j))) ∈ ℚ))
17. ∀x:{x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} 
      (λj.if (j =z i) then x else rat2real(fst((c j))) fi  ∈ |K|)
18. ∀x,y:{x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} .
      ((g (f (λj.if (j =z i) then x else rat2real(fst((c j))) fi )))
      = (g (f (λj.if (j =z i) then y else rat2real(fst((c j))) fi )))
      ∈ ℤ)
19. rat2real(fst((c i))) ∈ {x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} 
20. λj.if (j =z i) then rat2real(fst((c i))) else rat2real(fst((c j))) fi  ∈ |K|
21. ∀p:ℝ^k. ((¬¬in-rat-cube(k;p;c)) ⇒ (p ∈ |K|))
22. p : ℝ^k
23. ¬¬in-rat-cube(k;p;c)
24. x : |K|
25. y : |K|
26. (g (f x)) = (g (f y)) ∈ ℤ
27. req-vec(k;f x;λj.rat2real(fst((∂(K)[g (f y)] j))))
28. req-vec(k;f y;λj.rat2real(fst((∂(K)[g (f y)] j))))
⊢ f x ≡ f y

---

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{}x:|\mpartial{}(K)|.  \mexists{}i:\mBbbN{}||\mpartial{}(K)||.  req-vec(k;x;\mlambda{}j.rat2real(fst((\mpartial{}(K)[i]  j))))
8.  g  :  x:|\mpartial{}(K)|  {}\mrightarrow{}  \mBbbN{}||\mpartial{}(K)||
9.  \mforall{}x:|\mpartial{}(K)|.  req-vec(k;x;\mlambda{}j.rat2real(fst((\mpartial{}(K)[g  x]  j))))
10.  \mforall{}x,y:|\mpartial{}(K)|.    (x  \mequiv{}  y  {}\mRightarrow{}  ((g  x)  =  (g  y)))
11.  \mforall{}x,y:|K|.    (x  \mequiv{}  y  {}\mRightarrow{}  ((g  (f  x))  =  (g  (f  y))))
12.  c  :  \mBbbQ{}Cube(k)
13.  (c  \mmember{}  K)
14.  i  :  \mBbbN{}k
15.  fst((c  i))  <  snd((c  i))
16.  \mforall{}j:\mBbbN{}k.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  ((fst((c  j)))  =  (snd((c  j)))))
17.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [rat2real(fst((c  i))),  rat2real(snd((c  i)))]\} 
            (\mlambda{}j.if  (j  =\msubz{}  i)  then  x  else  rat2real(fst((c  j)))  fi    \mmember{}  |K|)
18.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [rat2real(fst((c  i))),  rat2real(snd((c  i)))]\}  .
            ((g  (f  (\mlambda{}j.if  (j  =\msubz{}  i)  then  x  else  rat2real(fst((c  j)))  fi  )))
            =  (g  (f  (\mlambda{}j.if  (j  =\msubz{}  i)  then  y  else  rat2real(fst((c  j)))  fi  ))))
19.  rat2real(fst((c  i)))  \mmember{}  \{x:\mBbbR{}|  x  \mmember{}  [rat2real(fst((c  i))),  rat2real(snd((c  i)))]\} 
20.  \mlambda{}j.if  (j  =\msubz{}  i)  then  rat2real(fst((c  i)))  else  rat2real(fst((c  j)))  fi    \mmember{}  |K|
21.  \mforall{}p:\mBbbR{}\^{}k.  ((\mneg{}\mneg{}in-rat-cube(k;p;c))  {}\mRightarrow{}  (p  \mmember{}  |K|))
22.  p  :  \mBbbR{}\^{}k
23.  \mneg{}\mneg{}in-rat-cube(k;p;c)
24.  x  :  |K|
25.  y  :  |K|
26.  (g  (f  x))  =  (g  (f  y))
\mvdash{}  f  x  \mequiv{}  f  y


By

---

Latex:
((Assert  req-vec(k;f  x;\mlambda{}j.rat2real(fst((\mpartial{}(K)[g  (f  x)]  j))))  BY
                Auto)
  THEN  (Assert  req-vec(k;f  y;\mlambda{}j.rat2real(fst((\mpartial{}(K)[g  (f  y)]  j))))  BY
                          Auto)
  THEN  HypSubst'  (-3)  (-2))

---

Home Index