---

Step * of Lemma m-cont-real-fun-is-mfun

∀[X:Type]. ∀[d:metric(X)]. ∀[f:X ⟶ ℝ].  (m-cont-real-fun(X;d;x.f[x]) ⇒ λx.f[x]:FUN(X;ℝ))
BY
{ (RepUR ``so_apply`` 0
   THEN Auto
   THEN D 0
   THEN Auto
   THEN RepUR ``so_apply rmetric meq`` 0
   THEN (Assert ⌜(f x1) = (f x2)⌝⋅ THENM (RWO "-1" 0 THEN Auto THEN nRNorm 0 THEN Auto))
   THEN RWO "req-iff-rabs-rleq" 0
   THEN Auto
   THEN (D 4 With ⌜(r1/r(m))⌝  THENA Auto)
   THEN ExRepD
   THEN InstHyp [⌜x1⌝;⌜x2⌝] (-1)⋅
   THEN Auto) }

1
.....antecedent..... 
1. X : Type
2. d : metric(X)
3. f : X ⟶ ℝ
4. x1 : X
5. x2 : X
6. x1 ≡ x2
7. m : ℕ+
8. delta : {e:ℝ| r0 < e} 
9. ∀x,x':X.  ((mdist(d;x;x') < delta) ⇒ (|(f x) - f x'| < (r1/r(m))))
⊢ mdist(d;x1;x2) < delta

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[f:X  {}\mrightarrow{}  \mBbbR{}].    (m-cont-real-fun(X;d;x.f[x])  {}\mRightarrow{}  \mlambda{}x.f[x]:FUN(X;\mBbbR{}))


By

---

Latex:
(RepUR  ``so\_apply``  0
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``so\_apply  rmetric  meq``  0
  THEN  (Assert  \mkleeneopen{}(f  x1)  =  (f  x2)\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1"  0  THEN  Auto  THEN  nRNorm  0  THEN  Auto))
  THEN  RWO  "req-iff-rabs-rleq"  0
  THEN  Auto
  THEN  (D  4  With  \mkleeneopen{}(r1/r(m))\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD
  THEN  InstHyp  [\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto)

---

Home Index