Step
*
2
2
1
1
1
1
of Lemma
real-cube-uniform-continuity
1. k : ℕ
2. n : ℤ
3. 2 ≤ n
4. ∀a,b:ℕn - 1 ⟶ ℝ.
((∀i:ℕn - 1. ((a i) < (b i)))
⇒ (∀f:{f:real-cube(n - 1;a;b) ⟶ ℝ^k| ∀x,y:real-cube(n - 1;a;b). (req-vec(n - 1;x;y) ⇒ req-vec(k;f x;f y))} .
∀e:{e:ℝ| r0 < e} .
∃d:ℕ+. ∀x,y:real-cube(n - 1;a;b). ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))))
5. a : ℕn ⟶ ℝ
6. b : ℕn ⟶ ℝ
7. ∀i:ℕn. ((a i) < (b i))
8. f : {f:real-cube(n;a;b) ⟶ ℝ^k| ∀x,y:real-cube(n;a;b). (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))}
9. e : {e:ℝ| r0 < e}
10. i : ℕn
11. t : {t:ℝ| t ∈ [a i, b i]}
12. ∀p:real-cube(n - 1;λj.if j <z i then a j else a (j + 1) fi ;λj.if j <z i then b j else b (j + 1) fi )
(λj.if j <z i then p j
if i <z j then p (j - 1)
else t
fi ∈ real-cube(n;a;b))
13. ∀e:{e:ℝ| r0 < e}
∃d:ℕ+
∀x,y:real-cube(n - 1;λj.if j <z i then a j else a (j + 1) fi ;λj.if j <z i then b j else b (j + 1) fi ).
((d(x;y) ≤ (r1/r(d)))
⇒ (d((λp.(f (λj.if j <z i then p j if i <z j then p (j - 1) else t fi ))) x;(λp.(f
(λj.if j <z i then p j
if i <z j then p (j - 1)
else t
fi )))
y) ≤ e))
⊢ ∃d:ℕ+. ∀x,y:{p:real-cube(n;a;b)| (p i) = t} . ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ (e/r(2))))
BY
{ ((D -1 With ⌜(e/r(2))⌝ THENW (DVar `e' THEN MemTypeCD THEN Auto THEN nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
THEN ParallelLast
THEN Auto) }
1
1. k : ℕ
2. n : ℤ
3. 2 ≤ n
4. ∀a,b:ℕn - 1 ⟶ ℝ.
((∀i:ℕn - 1. ((a i) < (b i)))
⇒ (∀f:{f:real-cube(n - 1;a;b) ⟶ ℝ^k| ∀x,y:real-cube(n - 1;a;b). (req-vec(n - 1;x;y) ⇒ req-vec(k;f x;f y))} .
∀e:{e:ℝ| r0 < e} .
∃d:ℕ+. ∀x,y:real-cube(n - 1;a;b). ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))))
5. a : ℕn ⟶ ℝ
6. b : ℕn ⟶ ℝ
7. ∀i:ℕn. ((a i) < (b i))
8. f : {f:real-cube(n;a;b) ⟶ ℝ^k| ∀x,y:real-cube(n;a;b). (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))}
9. e : {e:ℝ| r0 < e}
10. i : ℕn
11. t : {t:ℝ| t ∈ [a i, b i]}
12. ∀p:real-cube(n - 1;λj.if j <z i then a j else a (j + 1) fi ;λj.if j <z i then b j else b (j + 1) fi )
(λj.if j <z i then p j
if i <z j then p (j - 1)
else t
fi ∈ real-cube(n;a;b))
13. d : ℕ+
14. ∀x,y:real-cube(n - 1;λj.if j <z i then a j else a (j + 1) fi ;λj.if j <z i then b j else b (j + 1) fi ).
((d(x;y) ≤ (r1/r(d)))
⇒ (d((λp.(f (λj.if j <z i then p j if i <z j then p (j - 1) else t fi ))) x;(λp.(f
(λj.if j <z i then p j
if i <z j then p (j - 1)
else t
fi )))
y) ≤ (e/r(2))))
15. x : {p:real-cube(n;a;b)| (p i) = t}
16. y : {p:real-cube(n;a;b)| (p i) = t}
17. d(x;y) ≤ (r1/r(d))
⊢ d(f x;f y) ≤ (e/r(2))
Latex:
Latex:
1. k : \mBbbN{}
2. n : \mBbbZ{}
3. 2 \mleq{} n
4. \mforall{}a,b:\mBbbN{}n - 1 {}\mrightarrow{} \mBbbR{}.
((\mforall{}i:\mBbbN{}n - 1. ((a i) < (b i)))
{}\mRightarrow{} (\mforall{}f:\{f:real-cube(n - 1;a;b) {}\mrightarrow{} \mBbbR{}\^{}k|
\mforall{}x,y:real-cube(n - 1;a;b). (req-vec(n - 1;x;y) {}\mRightarrow{} req-vec(k;f x;f y))\} . \mforall{}e:\{e:\mBbbR{}|
r0 < e\} .
\mexists{}d:\mBbbN{}\msupplus{}. \mforall{}x,y:real-cube(n - 1;a;b). ((d(x;y) \mleq{} (r1/r(d))) {}\mRightarrow{} (d(f x;f y) \mleq{} e))))
5. a : \mBbbN{}n {}\mrightarrow{} \mBbbR{}
6. b : \mBbbN{}n {}\mrightarrow{} \mBbbR{}
7. \mforall{}i:\mBbbN{}n. ((a i) < (b i))
8. f : \{f:real-cube(n;a;b) {}\mrightarrow{} \mBbbR{}\^{}k| \mforall{}x,y:real-cube(n;a;b). (req-vec(n;x;y) {}\mRightarrow{} req-vec(k;f x;f y))\}
9. e : \{e:\mBbbR{}| r0 < e\}
10. i : \mBbbN{}n
11. t : \{t:\mBbbR{}| t \mmember{} [a i, b i]\}
12. \mforall{}p:real-cube(n - 1;\mlambda{}j.if j <z i then a j else a (j + 1) fi ;\mlambda{}j.if j <z i
then b j
else b (j + 1)
fi )
(\mlambda{}j.if j <z i then p j
if i <z j then p (j - 1)
else t
fi \mmember{} real-cube(n;a;b))
13. \mforall{}e:\{e:\mBbbR{}| r0 < e\}
\mexists{}d:\mBbbN{}\msupplus{}
\mforall{}x,y:real-cube(n - 1;\mlambda{}j.if j <z i then a j else a (j + 1) fi ;\mlambda{}j.if j <z i
then b j
else b (j + 1)
fi ).
((d(x;y) \mleq{} (r1/r(d)))
{}\mRightarrow{} (d((\mlambda{}p.(f (\mlambda{}j.if j <z i then p j if i <z j then p (j - 1) else t fi )))
x;(\mlambda{}p.(f (\mlambda{}j.if j <z i then p j if i <z j then p (j - 1) else t fi ))) y) \mleq{} e))
\mvdash{} \mexists{}d:\mBbbN{}\msupplus{}. \mforall{}x,y:\{p:real-cube(n;a;b)| (p i) = t\} . ((d(x;y) \mleq{} (r1/r(d))) {}\mRightarrow{} (d(f x;f y) \mleq{} (e/r(2))))
By
Latex:
((D -1 With \mkleeneopen{}(e/r(2))\mkleeneclose{} THENW (DVar `e' THEN MemTypeCD THEN Auto THEN nRMul \mkleeneopen{}r(2)\mkleeneclose{} 0\mcdot{} THEN Auto))
THEN ParallelLast
THEN Auto)
Home
Index