Step
*
1
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)))
12. λi.r0 ∈ B(n + 1)
13. p : S(n)
⊢ req-vec(n + 1;(λt.(g o (λp.t*p))) r1 p;p)
BY
{ (Reduce 0 THEN (Assert req-vec(n + 1;g r1*p;r1*p) BY BackThruSomeHyp)) }
1
.....aux.....
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)
⊢ ||r1*p|| = r1
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)
14. req-vec(n + 1;g r1*p;r1*p)
⊢ req-vec(n + 1;g r1*p;p)
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)))
12. \mlambda{}i.r0 \mmember{} B(n + 1)
13. p : S(n)
\mvdash{} req-vec(n + 1;(\mlambda{}t.(g o (\mlambda{}p.t*p))) r1 p;p)
By
Latex:
(Reduce 0 THEN (Assert req-vec(n + 1;g r1*p;r1*p) BY BackThruSomeHyp))
Home
Index