---

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


1. k : ℕ
2. a : ℕ0 ⟶ ℝ
3. b : ℕ0 ⟶ ℝ
4. ∀i:ℕ0. ((a i) < (b i))
5. f : {f:real-cube(0;a;b) ⟶ ℝ^k| ∀x,y:real-cube(0;a;b).  (req-vec(0;x;y) ⇒ req-vec(k;f x;f y))} 
6. e : {e:ℝ| r0 < e} 
⊢ ∃d:ℕ+. ∀x,y:real-cube(0;a;b).  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))
BY
{ ((Assert Top ⊆r real-cube(0;a;b) BY
          ((D 0 THENA Auto) THEN MemTypeCD THEN Auto THEN Unfold `real-vec` 0 THEN FunExt THEN Auto))
   THEN D 0 With ⌜1⌝ 
   THEN Auto
   THEN (Assert x = y ∈ real-cube(0;a;b) BY
               (SubsumeC ⌜Top⌝⋅ THEN Auto))
   THEN (RWO  "-1" 0 THENA Auto)
   THEN RWO "real-vec-dist-same-zero" 0
   THEN Auto
   THEN (Assert r0 < e BY
               Auto)
   THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  a  :  \mBbbN{}0  {}\mrightarrow{}  \mBbbR{}
3.  b  :  \mBbbN{}0  {}\mrightarrow{}  \mBbbR{}
4.  \mforall{}i:\mBbbN{}0.  ((a  i)  <  (b  i))
5.  f  :  \{f:real-cube(0;a;b)  {}\mrightarrow{}  \mBbbR{}\^{}k|  \mforall{}x,y:real-cube(0;a;b).    (req-vec(0;x;y)  {}\mRightarrow{}  req-vec(k;f  x;f  y))\} 
6.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
\mvdash{}  \mexists{}d:\mBbbN{}\msupplus{}.  \mforall{}x,y:real-cube(0;a;b).    ((d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  e))


By

---

Latex:
((Assert  Top  \msubseteq{}r  real-cube(0;a;b)  BY
                ((D  0  THENA  Auto)  THEN  MemTypeCD  THEN  Auto  THEN  Unfold  `real-vec`  0  THEN  FunExt  THEN  Auto))
  THEN  D  0  With  \mkleeneopen{}1\mkleeneclose{} 
  THEN  Auto
  THEN  (Assert  x  =  y  BY
                          (SubsumeC  \mkleeneopen{}Top\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (RWO    "-1"  0  THENA  Auto)
  THEN  RWO  "real-vec-dist-same-zero"  0
  THEN  Auto
  THEN  (Assert  r0  <  e  BY
                          Auto)
  THEN  Auto)

---

Home Index