---

Step * of Lemma interval-cube-uniform-continuity

∀I:{I:Interval| icompact(I)} 
  (iproper(I)
  ⇒ (∀n,k:ℕ. ∀f:{f:I^n ⟶ ℝ^k| ∀x,y:I^n.  (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))} . ∀e:{e:ℝ| r0 < e} .
        ∃d:ℕ+. ∀x,y:I^n.  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))))
BY
{ (Auto
   THEN (InstLemma `icompact-is-rccint` [⌜I⌝]⋅ THENA Auto)
   THEN (Assert icompact(I) BY
               Auto)
   THEN (D 2 THENA Auto)
   THEN HypSubst' 6 4
   THEN HypSubst' 6 0
   THEN (Assert real-cube(n;λj.left-endpoint(I);λj.right-endpoint(I)) ≡ [left-endpoint(I), right-endpoint(I)]^n BY
               ((RepeatFor 2 (D 0) THENA Auto) THEN D -1 THEN MemTypeCD THEN Auto))
   THEN (InstLemma `real-cube-uniform-continuity` [⌜k⌝;⌜n⌝;⌜λj.left-endpoint(I)⌝;⌜λj.right-endpoint(I)⌝;⌜f⌝;⌜e⌝]⋅
         THENA (Reduce 0 THEN Auto)
         )
   THEN RepeatFor 3 (ParallelLast)) }

---

Latex:

---

Latex:
\mforall{}I:\{I:Interval|  icompact(I)\} 
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}n,k:\mBbbN{}.  \mforall{}f:\{f:I\^{}n  {}\mrightarrow{}  \mBbbR{}\^{}k|  \mforall{}x,y:I\^{}n.    (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:I\^{}n.    ((d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  e))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `icompact-is-rccint`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  icompact(I)  BY
                          Auto)
  THEN  (D  2  THENA  Auto)
  THEN  HypSubst'  6  4
  THEN  HypSubst'  6  0
  THEN  (Assert  real-cube(n;\mlambda{}j.left-endpoint(I);\mlambda{}j.right-endpoint(I))  \mequiv{}
                            [left-endpoint(I),  right-endpoint(I)]\^{}n  BY
                          ((RepeatFor  2  (D  0)  THENA  Auto)  THEN  D  -1  THEN  MemTypeCD  THEN  Auto))
  THEN  (InstLemma  `real-cube-uniform-continuity`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}j.left-endpoint(I)\mkleeneclose{};
              \mkleeneopen{}\mlambda{}j.right-endpoint(I)\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
              THENA  (Reduce  0  THEN  Auto)
              )
  THEN  RepeatFor  3  (ParallelLast))

---

Home Index