Step
*
2
2
1
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. 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))
BY
{ ((D -4 With ⌜λj.if j <z i then x j else x (j + 1) fi ⌝
THENW (RepeatFor 2 (DVar `x')
THEN (MemTypeCD
THENL [(Unfold `real-vec` 0 THEN Auto); (Reduce 0 THEN (D 0 THENA Auto) THEN AutoSplit); Auto]
)
)
)
THEN (D -1 With ⌜λj.if j <z i then y j else y (j + 1) fi ⌝
THENW (RepeatFor 2 (DVar `y')
THEN (MemTypeCD
THENL [(Unfold `real-vec` 0 THEN Auto); (Reduce 0 THEN (D 0 THENA Auto) THEN AutoSplit); Auto]
)
)
)
THEN Reduce -1
THEN D -1) }
1
.....antecedent.....
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 : {p:real-cube(n;a;b)| (p i) = t}
15. y : {p:real-cube(n;a;b)| (p i) = t}
16. d(x;y) ≤ (r1/r(d))
⊢ d(λj.if j <z i then x j else x (j + 1) fi ;λj.if j <z i then y j else y (j + 1) fi ) ≤ (r1/r(d))
2
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 : {p:real-cube(n;a;b)| (p i) = t}
15. y : {p:real-cube(n;a;b)| (p i) = t}
16. d(x;y) ≤ (r1/r(d))
17. d(f
(λj.if j <z i then if j <z i then x j else x (j + 1) fi
if i <z j then if j - 1 <z i then x (j - 1) else x ((j - 1) + 1) fi
else t
fi );f
(λj.if j <z i then if j <z i then y j else y (j + 1) fi
if i <z j then if j - 1 <z i then y (j - 1) else y ((j - 1) + 1) fi
else t
fi )) ≤ (e/r(2))
⊢ 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. d : \mBbbN{}\msupplus{}
14. \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/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) \mleq{} (r1/r(d))
\mvdash{} d(f x;f y) \mleq{} (e/r(2))
By
Latex:
((D -4 With \mkleeneopen{}\mlambda{}j.if j <z i then x j else x (j + 1) fi \mkleeneclose{}
THENW (RepeatFor 2 (DVar `x')
THEN (MemTypeCD
THENL [(Unfold `real-vec` 0 THEN Auto)
; (Reduce 0 THEN (D 0 THENA Auto) THEN AutoSplit)
; Auto]
)
)
)
THEN (D -1 With \mkleeneopen{}\mlambda{}j.if j <z i then y j else y (j + 1) fi \mkleeneclose{}
THENW (RepeatFor 2 (DVar `y')
THEN (MemTypeCD
THENL [(Unfold `real-vec` 0 THEN Auto)
; (Reduce 0 THEN (D 0 THENA Auto) THEN AutoSplit)
; Auto]
)
)
)
THEN Reduce -1
THEN D -1)
Home
Index