---

Step * 2 2 2 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. d1 : ℕ+
11. ∀x,y:real-cube(n;a;b).  (((x 0) = (y 0)) ⇒ (d(x;y) ≤ (r1/r(d1))) ⇒ (d(f x;f y) ≤ (e/r(2))))
12. d : ℕ+
13. ∀x,y:real-cube(n;a;b).  (((x 1) = (y 1)) ⇒ (d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ (e/r(2))))
14. x : real-cube(n;a;b)
15. y : real-cube(n;a;b)
16. d(x;y) ≤ (r1/r(imax(d;d1)))
17. d ≤ imax(d;d1)
18. d1 ≤ imax(d;d1)
19. d(x;y) ≤ (r1/r(d))
20. d(x;y) ≤ (r1/r(d1))
⊢ d(f x;f y) ≤ e
BY
{ (Assert λj.if (j =z 0) then x 0 else y j fi  ∈ real-cube(n;a;b) BY
         (DVar `x' THEN DVar `y' THEN MemTypeCD THEN Try ((Unfold `real-vec` 0 THEN Auto)) THEN All Reduce 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. d1 : ℕ+
11. ∀x,y:real-cube(n;a;b).  (((x 0) = (y 0)) ⇒ (d(x;y) ≤ (r1/r(d1))) ⇒ (d(f x;f y) ≤ (e/r(2))))
12. d : ℕ+
13. ∀x,y:real-cube(n;a;b).  (((x 1) = (y 1)) ⇒ (d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ (e/r(2))))
14. x : real-cube(n;a;b)
15. y : real-cube(n;a;b)
16. d(x;y) ≤ (r1/r(imax(d;d1)))
17. d ≤ imax(d;d1)
18. d1 ≤ imax(d;d1)
19. d(x;y) ≤ (r1/r(d))
20. d(x;y) ≤ (r1/r(d1))
21. λj.if (j =z 0) then x 0 else y j fi  ∈ real-cube(n;a;b)
⊢ d(f x;f y) ≤ e

---

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.  d1  :  \mBbbN{}\msupplus{}
11.  \mforall{}x,y:real-cube(n;a;b).    (((x  0)  =  (y  0))  {}\mRightarrow{}  (d(x;y)  \mleq{}  (r1/r(d1)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  (e/r(2))))
12.  d  :  \mBbbN{}\msupplus{}
13.  \mforall{}x,y:real-cube(n;a;b).    (((x  1)  =  (y  1))  {}\mRightarrow{}  (d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  (e/r(2))))
14.  x  :  real-cube(n;a;b)
15.  y  :  real-cube(n;a;b)
16.  d(x;y)  \mleq{}  (r1/r(imax(d;d1)))
17.  d  \mleq{}  imax(d;d1)
18.  d1  \mleq{}  imax(d;d1)
19.  d(x;y)  \mleq{}  (r1/r(d))
20.  d(x;y)  \mleq{}  (r1/r(d1))
\mvdash{}  d(f  x;f  y)  \mleq{}  e


By

---

Latex:
(Assert  \mlambda{}j.if  (j  =\msubz{}  0)  then  x  0  else  y  j  fi    \mmember{}  real-cube(n;a;b)  BY
              (DVar  `x'
                THEN  DVar  `y'
                THEN  MemTypeCD
                THEN  Try  ((Unfold  `real-vec`  0  THEN  Auto))
                THEN  All  Reduce
                THEN  Auto))

---

Home Index