---

Step * of Lemma no-retraction-case-0

∀[k:ℕ]. ∀[K:0-dim-complex].  (0 < ||K|| ⇒ (¬retraction(|K|;rn-prod-metric(k);|∂(K)|)))
BY
{ (Intros
   THEN UseWitness ⌜λx.Ax⌝⋅
   THEN (Subst' ∂(K) ~ [] 0 THENA EAuto 1)
   THEN (Subst' |[]| ~ {p:ℝ^k| ¬¬(∃c∈[]. in-rat-cube(k;p;c))}  0
         THENA (RepUR ``rat-cube-complex-polyhedron stable-union`` 0 THEN Auto)
         )
   THEN Auto
   THEN Try (((D 0 THENA Auto) THEN Assert ⌜False⌝⋅ THEN Auto THEN D -1 THEN Auto THEN D -1 THEN All Reduce THEN Auto))
   THEN (Assert |K| BY
               EAuto 1)
   THEN RenameVar `p' (-1)) }

1
1. k : ℕ
2. K : 0-dim-complex
3. 0 < ||K||
4. retraction(|K|;rn-prod-metric(k);{p:ℝ^k| ¬¬(∃c∈[]. in-rat-cube(k;p;c))} )
5. p : |K|
⊢ False

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  UseWitness  \mkleeneopen{}\mlambda{}x.Ax\mkleeneclose{}\mcdot{}
  THEN  (Subst'  \mpartial{}(K)  \msim{}  []  0  THENA  EAuto  1)
  THEN  (Subst'  |[]|  \msim{}  \{p:\mBbbR{}\^{}k|  \mneg{}\mneg{}(\mexists{}c\mmember{}[].  in-rat-cube(k;p;c))\}    0
              THENA  (RepUR  ``rat-cube-complex-polyhedron  stable-union``  0  THEN  Auto)
              )
  THEN  Auto
  THEN  Try  (((D  0  THENA  Auto)
                        THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                        THEN  Auto
                        THEN  D  -1
                        THEN  Auto
                        THEN  D  -1
                        THEN  All  Reduce
                        THEN  Auto))
  THEN  (Assert  |K|  BY
                          EAuto  1)
  THEN  RenameVar  `p'  (-1))

---

Home Index