---

Step * 2 2 1 1 of Lemma real-cube-uniform-continuity

.....aux..... 
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. ∀f:{f: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 ) ⟶ ℝ^k| 
        ∀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 ).
          (req-vec(n - 1;x;y) ⇒ req-vec(k;f x;f y))} . ∀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(f x;f 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
{ (Assert ∀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)) BY
         ((D 0 THENA Auto)
          THEN (DVar `p' THEN Reduce -1)
          THEN ((MemTypeCD THEN Reduce 0)
                THENL [(Unfold `real-vec` 0 THEN Auto)
                      ; (((D 0 THENA Auto) THEN RenameVar `j' (-1))
                         THEN D 0
                         THEN (AutoSplit
                               THENL [(D -3 With ⌜j⌝  THEN Auto)
                                     ; (AutoSplit
                                        THENL [(D -4 With ⌜j - 1⌝  THEN Auto THEN SplitOnHypITE -2  THEN Auto)
                                              ; (Subst' j ~ i 0 THEN Auto)]
                                     )]
                         ))
                      ; 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. ∀f:{f: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 ) ⟶ ℝ^k| 
        ∀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 ).
          (req-vec(n - 1;x;y) ⇒ req-vec(k;f x;f y))} . ∀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(f x;f y) ≤ e))
13. ∀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))
⊢ ∃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))))

---

Latex:

---

Latex:
.....aux..... 
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{}f:\{f: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  )  {}\mrightarrow{}  \mBbbR{}\^{}k| 
                \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  ).
                    (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;\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(f  x;f  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:
(Assert  \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))  BY
              ((D  0  THENA  Auto)
                THEN  (DVar  `p'  THEN  Reduce  -1)
                THEN  ((MemTypeCD  THEN  Reduce  0)
                            THENL  [(Unfold  `real-vec`  0  THEN  Auto)
                                        ;  (((D  0  THENA  Auto)  THEN  RenameVar  `j'  (-1))
                                              THEN  D  0
                                              THEN  (AutoSplit
                                                          THENL  [(D  -3  With  \mkleeneopen{}j\mkleeneclose{}    THEN  Auto)
                                                                      ;  (AutoSplit
                                                                            THENL  [(D  -4  With  \mkleeneopen{}j  -  1\mkleeneclose{} 
                                                                                            THEN  Auto
                                                                                            THEN  SplitOnHypITE  -2 
                                                                                            THEN  Auto)
                                                                                        ;  (Subst'  j  \msim{}  i  0  THEN  Auto)]
                                                                      )]
                                              ))
                                        ;  Auto]
                )))

---

Home Index