---

Step * of Lemma real-cube-uniform-continuity

∀k,n:ℕ. ∀a,b:ℕn ⟶ ℝ.
  ((∀i:ℕn. ((a i) < (b i)))
  ⇒ (∀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))} . ∀e:{e:ℝ| r0 < e} \000C.
        ∃d:ℕ+. ∀x,y:real-cube(n;a;b).  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))))
BY
{ ((D 0 THENA Auto) THEN InductionOnNat THEN Auto) }

1
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))

2
1. k : ℕ
2. n : ℤ
3. [%1] : 0 < 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} 
⊢ ∃d:ℕ+. ∀x,y:real-cube(n;a;b).  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))

---

Latex:

---

Latex:
\mforall{}k,n:\mBbbN{}.  \mforall{}a,b:\mBbbN{}n  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}i:\mBbbN{}n.  ((a  i)  <  (b  i)))
    {}\mRightarrow{}  (\mforall{}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))\}  .  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
                \mexists{}d:\mBbbN{}\msupplus{}.  \mforall{}x,y:real-cube(n;a;b).    ((d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  e))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  InductionOnNat  THEN  Auto)

---

Home Index