---

Step * of Lemma mdist-m-cont

∀[X:Type]. ∀d:metric(X). ∀a:X.  m-cont-real-fun(X;d;x.mdist(d;a;x))
BY
{ (Auto THEN D 0 THEN Auto THEN D 0 With ⌜e⌝  THEN Auto THEN RWO "rabs-difference-bound-iff" 0 THEN Auto) }

1
1. [X] : Type
2. d : metric(X)
3. a : X
4. e : {e:ℝ| r0 < e} 
5. x : X
6. x' : X
7. mdist(d;x;x') < e
⊢ (mdist(d;a;x') - e) < mdist(d;a;x)

2
1. [X] : Type
2. d : metric(X)
3. a : X
4. e : {e:ℝ| r0 < e} 
5. x : X
6. x' : X
7. mdist(d;x;x') < e
8. (mdist(d;a;x') - e) < mdist(d;a;x)
⊢ mdist(d;a;x) < (mdist(d;a;x') + e)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}d:metric(X).  \mforall{}a:X.    m-cont-real-fun(X;d;x.mdist(d;a;x))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  D  0  With  \mkleeneopen{}e\mkleeneclose{} 
  THEN  Auto
  THEN  RWO  "rabs-difference-bound-iff"  0
  THEN  Auto)

---

Home Index