---

Step * 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. ∀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))))
⊢ ∀x,y:|∂(K)|.  (x ≡ y ⇒ ((g x) = (g y) ∈ ℤ))
BY
{ (Auto
   THEN (Assert req-vec(k;x;λj.rat2real(fst((∂(K)[g x] j)))) ∧ req-vec(k;y;λj.rat2real(fst((∂(K)[g y] j)))) BY
               Auto)
   ) }

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 : |∂(K)|
11. y : |∂(K)|
12. x ≡ y
13. req-vec(k;x;λj.rat2real(fst((∂(K)[g x] j)))) ∧ req-vec(k;y;λj.rat2real(fst((∂(K)[g y] j))))
⊢ (g x) = (g y) ∈ ℤ

---

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{}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))))
\mvdash{}  \mforall{}x,y:|\mpartial{}(K)|.    (x  \mequiv{}  y  {}\mRightarrow{}  ((g  x)  =  (g  y)))


By

---

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

---

Home Index