---

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


1. k : ℕ
2. n : ℤ
3. [%1] : 0 < 1
4. ∀a,b:ℕ1 - 1 ⟶ ℝ.
     ((∀i:ℕ1 - 1. ((a i) < (b i)))
     ⇒ (∀f:{f:real-cube(1 - 1;a;b) ⟶ ℝ^k| ∀x,y:real-cube(1 - 1;a;b).  (req-vec(1 - 1;x;y) ⇒ req-vec(k;f x;f y))} .
         ∀e:{e:ℝ| r0 < e} .
           ∃d:ℕ+. ∀x,y:real-cube(1 - 1;a;b).  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))))
5. a : ℕ1 ⟶ ℝ
6. b : ℕ1 ⟶ ℝ
7. ∀i:ℕ1. ((a i) < (b i))
8. f : {f:real-cube(1;a;b) ⟶ ℝ^k| ∀x,y:real-cube(1;a;b).  (req-vec(1;x;y) ⇒ req-vec(k;f x;f y))} 
9. e : {e:ℝ| r0 < e} 
10. n = 1 ∈ ℤ
11. ∀x:{x:ℝ| x ∈ [a 0, b 0]} . (λu.x ∈ real-cube(1;a;b))
12. ∀f:[a 0, b 0] ⟶ℝ. (real-fun(f;a 0;b 0) ⇐⇒ real-cont(f;a 0;b 0))
13. ∀i:ℕk. real-cont(λt.(f (λu.t) i);a 0;b 0)
14. ∀i:ℕk. ∃d:{d:ℝ| r0 < d} . ∀x,y:{t:ℝ| t ∈ [a 0, b 0]} .  ((|x - y| ≤ d) ⇒ (|(f (λu.x) i) - f (λu.y) i| ≤ (e/r(k))))
15. d : i:ℕk ⟶ {d:ℝ| r0 < d} 
16. ∀i:ℕk. ∀x,y:{t:ℝ| t ∈ [a 0, b 0]} .  ((|x - y| ≤ (d i)) ⇒ (|(f (λu.x) i) - f (λu.y) i| ≤ (e/r(k))))
17. ∃md:{d:ℝ| r0 < d} . ∀i:ℕk. (md ≤ (d i))
⊢ ∃d:ℕ+. ∀x,y:real-cube(1;a;b).  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))
BY
{ (D -1 THEN (InstLemma `small-reciprocal-real` [⌜md⌝]⋅ THENA Auto) THEN ParallelLast THEN Auto) }

1
1. k : ℕ
2. n : ℤ
3. 0 < 1
4. ∀a,b:ℕ1 - 1 ⟶ ℝ.
     ((∀i:ℕ1 - 1. ((a i) < (b i)))
     ⇒ (∀f:{f:real-cube(1 - 1;a;b) ⟶ ℝ^k| ∀x,y:real-cube(1 - 1;a;b).  (req-vec(1 - 1;x;y) ⇒ req-vec(k;f x;f y))} .
         ∀e:{e:ℝ| r0 < e} .
           ∃d:ℕ+. ∀x,y:real-cube(1 - 1;a;b).  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))))
5. a : ℕ1 ⟶ ℝ
6. b : ℕ1 ⟶ ℝ
7. ∀i:ℕ1. ((a i) < (b i))
8. f : {f:real-cube(1;a;b) ⟶ ℝ^k| ∀x,y:real-cube(1;a;b).  (req-vec(1;x;y) ⇒ req-vec(k;f x;f y))} 
9. e : {e:ℝ| r0 < e} 
10. n = 1 ∈ ℤ
11. ∀x:{x:ℝ| x ∈ [a 0, b 0]} . (λu.x ∈ real-cube(1;a;b))
12. ∀f:[a 0, b 0] ⟶ℝ. (real-fun(f;a 0;b 0) ⇐⇒ real-cont(f;a 0;b 0))
13. ∀i:ℕk. real-cont(λt.(f (λu.t) i);a 0;b 0)
14. ∀i:ℕk. ∃d:{d:ℝ| r0 < d} . ∀x,y:{t:ℝ| t ∈ [a 0, b 0]} .  ((|x - y| ≤ d) ⇒ (|(f (λu.x) i) - f (λu.y) i| ≤ (e/r(k))))
15. d : i:ℕk ⟶ {d:ℝ| r0 < d} 
16. ∀i:ℕk. ∀x,y:{t:ℝ| t ∈ [a 0, b 0]} .  ((|x - y| ≤ (d i)) ⇒ (|(f (λu.x) i) - f (λu.y) i| ≤ (e/r(k))))
17. md : {d:ℝ| r0 < d} 
18. ∀i:ℕk. (md ≤ (d i))
19. k1 : ℕ+
20. (r1/r(k1)) < md
21. x : real-cube(1;a;b)
22. y : real-cube(1;a;b)
23. d(x;y) ≤ (r1/r(k1))
⊢ d(f x;f y) ≤ e

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbZ{}
3.  [\%1]  :  0  <  1
4.  \mforall{}a,b:\mBbbN{}1  -  1  {}\mrightarrow{}  \mBbbR{}.
          ((\mforall{}i:\mBbbN{}1  -  1.  ((a  i)  <  (b  i)))
          {}\mRightarrow{}  (\mforall{}f:\{f:real-cube(1  -  1;a;b)  {}\mrightarrow{}  \mBbbR{}\^{}k| 
                          \mforall{}x,y:real-cube(1  -  1;a;b).    (req-vec(1  -  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(1  -  1;a;b).    ((d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  e))))
5.  a  :  \mBbbN{}1  {}\mrightarrow{}  \mBbbR{}
6.  b  :  \mBbbN{}1  {}\mrightarrow{}  \mBbbR{}
7.  \mforall{}i:\mBbbN{}1.  ((a  i)  <  (b  i))
8.  f  :  \{f:real-cube(1;a;b)  {}\mrightarrow{}  \mBbbR{}\^{}k|  \mforall{}x,y:real-cube(1;a;b).    (req-vec(1;x;y)  {}\mRightarrow{}  req-vec(k;f  x;f  y))\} 
9.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
10.  n  =  1
11.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a  0,  b  0]\}  .  (\mlambda{}u.x  \mmember{}  real-cube(1;a;b))
12.  \mforall{}f:[a  0,  b  0]  {}\mrightarrow{}\mBbbR{}.  (real-fun(f;a  0;b  0)  \mLeftarrow{}{}\mRightarrow{}  real-cont(f;a  0;b  0))
13.  \mforall{}i:\mBbbN{}k.  real-cont(\mlambda{}t.(f  (\mlambda{}u.t)  i);a  0;b  0)
14.  \mforall{}i:\mBbbN{}k
            \mexists{}d:\{d:\mBbbR{}|  r0  <  d\} 
              \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  [a  0,  b  0]\}  .    ((|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  (|(f  (\mlambda{}u.x)  i)  -  f  (\mlambda{}u.y)  i|  \mleq{}  (e/r(k))))
15.  d  :  i:\mBbbN{}k  {}\mrightarrow{}  \{d:\mBbbR{}|  r0  <  d\} 
16.  \mforall{}i:\mBbbN{}k.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  [a  0,  b  0]\}  .
            ((|x  -  y|  \mleq{}  (d  i))  {}\mRightarrow{}  (|(f  (\mlambda{}u.x)  i)  -  f  (\mlambda{}u.y)  i|  \mleq{}  (e/r(k))))
17.  \mexists{}md:\{d:\mBbbR{}|  r0  <  d\}  .  \mforall{}i:\mBbbN{}k.  (md  \mleq{}  (d  i))
\mvdash{}  \mexists{}d:\mBbbN{}\msupplus{}.  \mforall{}x,y:real-cube(1;a;b).    ((d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  e))


By

---

Latex:
(D  -1  THEN  (InstLemma  `small-reciprocal-real`  [\mkleeneopen{}md\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ParallelLast  THEN  Auto)

---

Home Index