Step
*
1
2
1
1
1
1
of Lemma
NoBallRetraction-implies-BrouwerFPT
1. n : ℕ
2. f : B(n) ⟶ B(n)
3. ∀x,y:B(n). (req-vec(n;x;y) ⇒ req-vec(n;f x;f y))
4. ∀x:B(n). f x ≠ x
5. ¬(n = 0 ∈ ℤ)
6. ∀x:B(n). (r0 < x - f x⋅x - f x)
7. ∀x:B(n). ((f x⋅f x - r1) ≤ r0)
8. ∀x:B(n). (r0 ≤ x - f x⋅x - f x)
9. ∀x:B(n). ∀b:ℝ. (r0 ≤ ((b * b) - r(4) * x - f x⋅x - f x * (f x⋅f x - r1)))
10. ∀x:B(n). (||f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x - r1)*x - f x|| = r1)
11. ∀x,y:B(n).
(req-vec(n;x;y)
⇒ req-vec(n;f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x
- r1)*x - f x;f y + quadratic1(y - f y⋅y - f y;r(2) * f y⋅y - f y;f y⋅f y - r1)*y - f y))
⊢ ∃g:B(n) ⟶ B(n)
((∀x,y:B(n). (req-vec(n;x;y) ⇒ req-vec(n;g x;g y)))
∧ (∀x:B(n). (||g x|| = r1))
∧ (∀x:B(n). ((||x|| = r1) ⇒ req-vec(n;g x;x))))
BY
{ (D 0 With ⌜λx.f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x - r1)*x - f x⌝ THEN Reduce 0 THEN Auto) }
1
1. n : ℕ
2. f : B(n) ⟶ B(n)
3. ∀x,y:B(n). (req-vec(n;x;y) ⇒ req-vec(n;f x;f y))
4. ∀x:B(n). f x ≠ x
5. ¬(n = 0 ∈ ℤ)
6. ∀x:B(n). (r0 < x - f x⋅x - f x)
7. ∀x:B(n). ((f x⋅f x - r1) ≤ r0)
8. ∀x:B(n). (r0 ≤ x - f x⋅x - f x)
9. ∀x:B(n). ∀b:ℝ. (r0 ≤ ((b * b) - r(4) * x - f x⋅x - f x * (f x⋅f x - r1)))
10. ∀x:B(n). (||f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x - r1)*x - f x|| = r1)
11. ∀x,y:B(n).
(req-vec(n;x;y)
⇒ req-vec(n;f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x
- r1)*x - f x;f y + quadratic1(y - f y⋅y - f y;r(2) * f y⋅y - f y;f y⋅f y - r1)*y - f y))
12. x : B(n)
⊢ f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x - r1)*x - f x ∈ B(n)
2
1. n : ℕ
2. f : B(n) ⟶ B(n)
3. ∀x,y:B(n). (req-vec(n;x;y) ⇒ req-vec(n;f x;f y))
4. ∀x:B(n). f x ≠ x
5. ¬(n = 0 ∈ ℤ)
6. ∀x:B(n). (r0 < x - f x⋅x - f x)
7. ∀x:B(n). ((f x⋅f x - r1) ≤ r0)
8. ∀x:B(n). (r0 ≤ x - f x⋅x - f x)
9. ∀x:B(n). ∀b:ℝ. (r0 ≤ ((b * b) - r(4) * x - f x⋅x - f x * (f x⋅f x - r1)))
10. ∀x:B(n). (||f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x - r1)*x - f x|| = r1)
11. ∀x,y:B(n).
(req-vec(n;x;y)
⇒ req-vec(n;f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x
- r1)*x - f x;f y + quadratic1(y - f y⋅y - f y;r(2) * f y⋅y - f y;f y⋅f y - r1)*y - f y))
12. ∀x,y:B(n).
(req-vec(n;x;y)
⇒ req-vec(n;f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x
- r1)*x - f x;f y + quadratic1(y - f y⋅y - f y;r(2) * f y⋅y - f y;f y⋅f y - r1)*y - f y))
13. ∀x:B(n). (||f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x - r1)*x - f x|| = r1)
14. x : B(n)
15. ||x|| = r1
⊢ req-vec(n;f x + quadratic1(x - f x⋅x - f x;r(2) * f x⋅x - f x;f x⋅f x - r1)*x - f x;x)
Latex:
Latex:
1. n : \mBbbN{}
2. f : B(n) {}\mrightarrow{} B(n)
3. \mforall{}x,y:B(n). (req-vec(n;x;y) {}\mRightarrow{} req-vec(n;f x;f y))
4. \mforall{}x:B(n). f x \mneq{} x
5. \mneg{}(n = 0)
6. \mforall{}x:B(n). (r0 < x - f x\mcdot{}x - f x)
7. \mforall{}x:B(n). ((f x\mcdot{}f x - r1) \mleq{} r0)
8. \mforall{}x:B(n). (r0 \mleq{} x - f x\mcdot{}x - f x)
9. \mforall{}x:B(n). \mforall{}b:\mBbbR{}. (r0 \mleq{} ((b * b) - r(4) * x - f x\mcdot{}x - f x * (f x\mcdot{}f x - r1)))
10. \mforall{}x:B(n). (||f x + quadratic1(x - f x\mcdot{}x - f x;r(2) * f x\mcdot{}x - f x;f x\mcdot{}f x - r1)*x - f x|| = r1)
11. \mforall{}x,y:B(n).
(req-vec(n;x;y)
{}\mRightarrow{} req-vec(n;f x + quadratic1(x - f x\mcdot{}x - f x;r(2) * f x\mcdot{}x - f x;f x\mcdot{}f x
- r1)*x - f x;f y + quadratic1(y - f y\mcdot{}y - f y;r(2) * f y\mcdot{}y - f y;f y\mcdot{}f y - r1)*y - f y))
\mvdash{} \mexists{}g:B(n) {}\mrightarrow{} B(n)
((\mforall{}x,y:B(n). (req-vec(n;x;y) {}\mRightarrow{} req-vec(n;g x;g y)))
\mwedge{} (\mforall{}x:B(n). (||g x|| = r1))
\mwedge{} (\mforall{}x:B(n). ((||x|| = r1) {}\mRightarrow{} req-vec(n;g x;x))))
By
Latex:
(D 0 With \mkleeneopen{}\mlambda{}x.f x + quadratic1(x - f x\mcdot{}x - f x;r(2) * f x\mcdot{}x - f x;f x\mcdot{}f x - r1)*x - f x\mkleeneclose{}
THEN Reduce 0
THEN Auto)
Home
Index