---

Step * 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 : |∂(K)|
11. y : |∂(K)|
12. req-vec(k;x;y)
13. req-vec(k;x;λj.rat2real(fst((∂(K)[g x] j))))
14. req-vec(k;y;λj.rat2real(fst((∂(K)[g y] j))))
15. ¬((g x) = (g y) ∈ ℤ)
⊢ False
BY
{ (RepeatFor 4 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜g x⌝;⌜g y⌝]⋅
   THEN RepeatFor 2 ((Thin (-1) THEN MoveToConcl (-1)))
   THEN (GenConclTerm ⌜∂(K)⌝⋅ THENA Auto)
   THEN DVar `y'
   THEN DVar `x'
   THEN All Thin
   THEN Reduce -1
   THEN D -1
   THEN Auto) }

1
1. k : ℕ
2. x : ℝ^k
3. y : ℝ^k
4. v : ℚCube(k) List
5. no_repeats(ℚCube(k);v)
6. (∀c,d∈v.  Compatible(c;d))
7. (∀c∈v.dim(c) = 0 ∈ ℤ)
8. v@0 : ℕ||v||
9. v1 : ℕ||v||
10. req-vec(k;x;y)
11. req-vec(k;x;λj.rat2real(fst((v[v@0] j))))
12. req-vec(k;y;λj.rat2real(fst((v[v1] j))))
13. ¬(v@0 = v1 ∈ ℤ)
⊢ False

---

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.  x  :  |\mpartial{}(K)|
11.  y  :  |\mpartial{}(K)|
12.  req-vec(k;x;y)
13.  req-vec(k;x;\mlambda{}j.rat2real(fst((\mpartial{}(K)[g  x]  j))))
14.  req-vec(k;y;\mlambda{}j.rat2real(fst((\mpartial{}(K)[g  y]  j))))
15.  \mneg{}((g  x)  =  (g  y))
\mvdash{}  False


By

---

Latex:
(RepeatFor  4  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}g  x\mkleeneclose{};\mkleeneopen{}g  y\mkleeneclose{}]\mcdot{}
  THEN  RepeatFor  2  ((Thin  (-1)  THEN  MoveToConcl  (-1)))
  THEN  (GenConclTerm  \mkleeneopen{}\mpartial{}(K)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  DVar  `y'
  THEN  DVar  `x'
  THEN  All  Thin
  THEN  Reduce  -1
  THEN  D  -1
  THEN  Auto)

---

Home Index