Step * 1 1 of Lemma IdNotHomotopicConst-implies-BrowerFPT


1. : ℕ
2. IdNotHomotopicConst(n)
3. B(n 1) ⟶ B(n 1)
4. ∀x,y:B(n 1).  (req-vec(n 1;x;y)  req-vec(n 1;g x;g y))
5. ∀x:B(n 1). (||g x|| r1)
6. ∀x:B(n 1). ((||x|| r1)  req-vec(n 1;g x;x))
7. ∀h:{h:B(n 1) ⟶ B(n 1)| ∀p,q:B(n 1).  (req-vec(n 1;p;q)  req-vec(n 1;h p;h q))} (g h ∈ sphere-map(n))
⊢ False
BY
((Assert ∀t:{t:ℝt ∈ [r0, r1]} . ∀p:B(n 1).  (t*p ∈ B(n 1)) BY
          (Auto
           THEN -1
           THEN DSetVars
           THEN MemTypeCD
           THEN Auto
           THEN RWO  "real-vec-norm-mul" 0
           THEN Auto
           THEN nRMul ⌜|t|⌝ (-1)⋅
           THEN (RWO "-1" THENA Auto)
           THEN RWO "rabs-of-nonneg" 0
           THEN Auto))
   THEN (Assert ∀t:{t:ℝt ∈ [r0, r1]} p.t*p ∈ B(n 1) ⟶ B(n 1)) BY
               ((D THENM FunExt THENM Reduce 0) THEN Auto))
   }

1
1. : ℕ
2. IdNotHomotopicConst(n)
3. B(n 1) ⟶ B(n 1)
4. ∀x,y:B(n 1).  (req-vec(n 1;x;y)  req-vec(n 1;g x;g y))
5. ∀x:B(n 1). (||g x|| r1)
6. ∀x:B(n 1). ((||x|| r1)  req-vec(n 1;g x;x))
7. ∀h:{h:B(n 1) ⟶ B(n 1)| ∀p,q:B(n 1).  (req-vec(n 1;p;q)  req-vec(n 1;h p;h q))} (g h ∈ sphere-map(n))
8. ∀t:{t:ℝt ∈ [r0, r1]} . ∀p:B(n 1).  (t*p ∈ B(n 1))
9. ∀t:{t:ℝt ∈ [r0, r1]} p.t*p ∈ B(n 1) ⟶ B(n 1))
⊢ False


Latex:


Latex:

1.  n  :  \mBbbN{}
2.  IdNotHomotopicConst(n)
3.  g  :  B(n  +  1)  {}\mrightarrow{}  B(n  +  1)
4.  \mforall{}x,y:B(n  +  1).    (req-vec(n  +  1;x;y)  {}\mRightarrow{}  req-vec(n  +  1;g  x;g  y))
5.  \mforall{}x:B(n  +  1).  (||g  x||  =  r1)
6.  \mforall{}x:B(n  +  1).  ((||x||  =  r1)  {}\mRightarrow{}  req-vec(n  +  1;g  x;x))
7.  \mforall{}h:\{h:B(n  +  1)  {}\mrightarrow{}  B(n  +  1)|  \mforall{}p,q:B(n  +  1).    (req-vec(n  +  1;p;q)  {}\mRightarrow{}  req-vec(n  +  1;h  p;h  q))\} 
          (g  o  h  \mmember{}  sphere-map(n))
\mvdash{}  False


By


Latex:
((Assert  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  .  \mforall{}p:B(n  +  1).    (t*p  \mmember{}  B(n  +  1))  BY
                (Auto
                  THEN  D  -1
                  THEN  DSetVars
                  THEN  MemTypeCD
                  THEN  Auto
                  THEN  RWO    "real-vec-norm-mul"  0
                  THEN  Auto
                  THEN  nRMul  \mkleeneopen{}|t|\mkleeneclose{}  (-1)\mcdot{}
                  THEN  (RWO  "-1"  0  THENA  Auto)
                  THEN  RWO  "rabs-of-nonneg"  0
                  THEN  Auto))
  THEN  (Assert  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  .  (\mlambda{}p.t*p  \mmember{}  B(n  +  1)  {}\mrightarrow{}  B(n  +  1))  BY
                          ((D  0  THENM  FunExt  THENM  Reduce  0)  THEN  Auto))
  )




Home Index