Step
*
1
1
1
1
1
1
of Lemma
IdNotHomotopicConst-implies-BrowerFPT
1. n : ℕ
2. g : B(n + 1) ⟶ B(n + 1)
3. ∀x,y:B(n + 1). (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))
4. ∀x:B(n + 1). (||g x|| = r1)
5. ∀x:B(n + 1). ((||x|| = r1) ⇒ req-vec(n + 1;g x;x))
6. ∀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 o h ∈ sphere-map(n))
7. ∀t:{t:ℝ| t ∈ [r0, r1]} . ∀p:B(n + 1). (t*p ∈ B(n + 1))
8. ∀t:{t:ℝ| t ∈ [r0, r1]} . (λp.t*p ∈ B(n + 1) ⟶ B(n + 1))
9. ∀t:{t:ℝ| t ∈ [r0, r1]}
(λp.t*p ∈ {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))} )
10. ∀t:{t:ℝ| t ∈ [r0, r1]} . (g o (λp.t*p) ∈ sphere-map(n))
11. ∀t,s:{t:ℝ| t ∈ [r0, r1]} . ((t = s) ⇒ sphere-map-eq(n;g o (λp.t*p);g o (λp.s*p)))
⊢ ∃h:{t:ℝ| t ∈ [r0, r1]} ⟶ S(n) ⟶ S(n)
((∀p:S(n). req-vec(n + 1;h r1 p;p))
∧ (∃q:S(n). ∀p:S(n). req-vec(n + 1;h r0 p;q))
∧ (∀t1,t2:{t:ℝ| t ∈ [r0, r1]} . ∀p1,p2:S(n). ((t1 = t2) ⇒ req-vec(n + 1;p1;p2) ⇒ req-vec(n + 1;h t1 p1;h t2 p2))))
BY
{ ((Assert λi.r0 ∈ B(n + 1) BY
(MemTypeCD THEN Auto THEN RWO "real-vec-norm-0" 0 THEN Auto))
THEN D 0 With ⌜λt.(g o (λp.t*p))⌝
THEN Auto) }
1
1. n : ℕ
2. g : B(n + 1) ⟶ B(n + 1)
3. ∀x,y:B(n + 1). (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))
4. ∀x:B(n + 1). (||g x|| = r1)
5. ∀x:B(n + 1). ((||x|| = r1) ⇒ req-vec(n + 1;g x;x))
6. ∀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 o h ∈ sphere-map(n))
7. ∀t:{t:ℝ| t ∈ [r0, r1]} . ∀p:B(n + 1). (t*p ∈ B(n + 1))
8. ∀t:{t:ℝ| t ∈ [r0, r1]} . (λp.t*p ∈ B(n + 1) ⟶ B(n + 1))
9. ∀t:{t:ℝ| t ∈ [r0, r1]}
(λp.t*p ∈ {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))} )
10. ∀t:{t:ℝ| t ∈ [r0, r1]} . (g o (λp.t*p) ∈ sphere-map(n))
11. ∀t,s:{t:ℝ| t ∈ [r0, r1]} . ((t = s) ⇒ sphere-map-eq(n;g o (λp.t*p);g o (λp.s*p)))
12. λi.r0 ∈ B(n + 1)
13. p : S(n)
⊢ req-vec(n + 1;(λt.(g o (λp.t*p))) r1 p;p)
2
1. n : ℕ
2. g : B(n + 1) ⟶ B(n + 1)
3. ∀x,y:B(n + 1). (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))
4. ∀x:B(n + 1). (||g x|| = r1)
5. ∀x:B(n + 1). ((||x|| = r1) ⇒ req-vec(n + 1;g x;x))
6. ∀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 o h ∈ sphere-map(n))
7. ∀t:{t:ℝ| t ∈ [r0, r1]} . ∀p:B(n + 1). (t*p ∈ B(n + 1))
8. ∀t:{t:ℝ| t ∈ [r0, r1]} . (λp.t*p ∈ B(n + 1) ⟶ B(n + 1))
9. ∀t:{t:ℝ| t ∈ [r0, r1]}
(λp.t*p ∈ {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))} )
10. ∀t:{t:ℝ| t ∈ [r0, r1]} . (g o (λp.t*p) ∈ sphere-map(n))
11. ∀t,s:{t:ℝ| t ∈ [r0, r1]} . ((t = s) ⇒ sphere-map-eq(n;g o (λp.t*p);g o (λp.s*p)))
12. λi.r0 ∈ B(n + 1)
13. ∀p:S(n). req-vec(n + 1;(λt.(g o (λp.t*p))) r1 p;p)
⊢ ∃q:S(n). ∀p:S(n). req-vec(n + 1;(λt.(g o (λp.t*p))) r0 p;q)
3
1. n : ℕ
2. g : B(n + 1) ⟶ B(n + 1)
3. ∀x,y:B(n + 1). (req-vec(n + 1;x;y) ⇒ req-vec(n + 1;g x;g y))
4. ∀x:B(n + 1). (||g x|| = r1)
5. ∀x:B(n + 1). ((||x|| = r1) ⇒ req-vec(n + 1;g x;x))
6. ∀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 o h ∈ sphere-map(n))
7. ∀t:{t:ℝ| t ∈ [r0, r1]} . ∀p:B(n + 1). (t*p ∈ B(n + 1))
8. ∀t:{t:ℝ| t ∈ [r0, r1]} . (λp.t*p ∈ B(n + 1) ⟶ B(n + 1))
9. ∀t:{t:ℝ| t ∈ [r0, r1]}
(λp.t*p ∈ {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))} )
10. ∀t:{t:ℝ| t ∈ [r0, r1]} . (g o (λp.t*p) ∈ sphere-map(n))
11. ∀t,s:{t:ℝ| t ∈ [r0, r1]} . ((t = s) ⇒ sphere-map-eq(n;g o (λp.t*p);g o (λp.s*p)))
12. λi.r0 ∈ B(n + 1)
13. ∀p:S(n). req-vec(n + 1;(λt.(g o (λp.t*p))) r1 p;p)
14. ∃q:S(n). ∀p:S(n). req-vec(n + 1;(λt.(g o (λp.t*p))) r0 p;q)
15. t1 : {t:ℝ| t ∈ [r0, r1]}
16. t2 : {t:ℝ| t ∈ [r0, r1]}
17. p1 : S(n)
18. p2 : S(n)
19. t1 = t2
20. req-vec(n + 1;p1;p2)
⊢ req-vec(n + 1;(λt.(g o (λp.t*p))) t1 p1;(λt.(g o (λp.t*p))) t2 p2)
Latex:
Latex:
1. n : \mBbbN{}
2. g : B(n + 1) {}\mrightarrow{} B(n + 1)
3. \mforall{}x,y:B(n + 1). (req-vec(n + 1;x;y) {}\mRightarrow{} req-vec(n + 1;g x;g y))
4. \mforall{}x:B(n + 1). (||g x|| = r1)
5. \mforall{}x:B(n + 1). ((||x|| = r1) {}\mRightarrow{} req-vec(n + 1;g x;x))
6. \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))
7. \mforall{}t:\{t:\mBbbR{}| t \mmember{} [r0, r1]\} . \mforall{}p:B(n + 1). (t*p \mmember{} B(n + 1))
8. \mforall{}t:\{t:\mBbbR{}| t \mmember{} [r0, r1]\} . (\mlambda{}p.t*p \mmember{} B(n + 1) {}\mrightarrow{} B(n + 1))
9. \mforall{}t:\{t:\mBbbR{}| t \mmember{} [r0, r1]\}
(\mlambda{}p.t*p \mmember{} \{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))\} )
10. \mforall{}t:\{t:\mBbbR{}| t \mmember{} [r0, r1]\} . (g o (\mlambda{}p.t*p) \mmember{} sphere-map(n))
11. \mforall{}t,s:\{t:\mBbbR{}| t \mmember{} [r0, r1]\} . ((t = s) {}\mRightarrow{} sphere-map-eq(n;g o (\mlambda{}p.t*p);g o (\mlambda{}p.s*p)))
\mvdash{} \mexists{}h:\{t:\mBbbR{}| t \mmember{} [r0, r1]\} {}\mrightarrow{} S(n) {}\mrightarrow{} S(n)
((\mforall{}p:S(n). req-vec(n + 1;h r1 p;p))
\mwedge{} (\mexists{}q:S(n). \mforall{}p:S(n). req-vec(n + 1;h r0 p;q))
\mwedge{} (\mforall{}t1,t2:\{t:\mBbbR{}| t \mmember{} [r0, r1]\} . \mforall{}p1,p2:S(n).
((t1 = t2) {}\mRightarrow{} req-vec(n + 1;p1;p2) {}\mRightarrow{} req-vec(n + 1;h t1 p1;h t2 p2))))
By
Latex:
((Assert \mlambda{}i.r0 \mmember{} B(n + 1) BY
(MemTypeCD THEN Auto THEN RWO "real-vec-norm-0" 0 THEN Auto))
THEN D 0 With \mkleeneopen{}\mlambda{}t.(g o (\mlambda{}p.t*p))\mkleeneclose{}
THEN Auto)
Home
Index