---

Step * of Lemma no-retraction-case-1

∀[k:ℕ]. ∀[K:1-dim-complex].  (0 < ||K|| ⇒ (¬retraction(|K|;rn-prod-metric(k);|∂(K)|)))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN (InstLemma `0-dim-complex-polyhedron` [⌜k⌝;⌜∂(K)⌝]⋅ THENA Auto)
   THEN (Skolemize (-1) `g'
         THENA ((D 0
                 THENL [Auto
                       ; ((GenConclTerm ⌜g1 x⌝⋅ THENA Auto)
                          THEN Thin (-1)
                          THEN MoveToConcl (-1)
                          THEN (GenConclTerm ⌜∂(K)⌝⋅ THENA Auto)
                          THEN D -2
                          THEN Auto)]
                )
               ORELSE 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))))
⊢ False

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[K:1-dim-complex].    (0  <  ||K||  {}\mRightarrow{}  (\mneg{}retraction(|K|;rn-prod-metric(k);|\mpartial{}(K)|)))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  (InstLemma  `0-dim-complex-polyhedron`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mpartial{}(K)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Skolemize  (-1)  `g'
              THENA  ((D  0
                              THENL  [Auto
                                          ;  ((GenConclTerm  \mkleeneopen{}g1  x\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                THEN  Thin  (-1)
                                                THEN  MoveToConcl  (-1)
                                                THEN  (GenConclTerm  \mkleeneopen{}\mpartial{}(K)\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                THEN  D  -2
                                                THEN  Auto)]
                            )
                          ORELSE  Auto
                          )
              ))

---

Home Index