---

Step * of Lemma mdist-difference2

∀[X:Type]. ∀[d:metric(X)]. ∀[x,a,b,y:X].  (|mdist(d;x;y) - mdist(d;a;b)| ≤ (mdist(d;x;a) + mdist(d;y;b)))
BY
{ ((Auto THEN UseTriangleInequality [⌜mdist(d;x;b)⌝]⋅)
   THEN (RWO "mdist-difference" 0 THENA Auto)
   THEN (RWO "mdist-symm" 0 THENA Auto)
   THEN (RWO "mdist-difference" 0 THENA Auto)
   THEN nRAdd ⌜-(mdist(d;b;y))⌝ 0⋅
   THEN BLemma `rleq_weakening`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[x,a,b,y:X].
    (|mdist(d;x;y)  -  mdist(d;a;b)|  \mleq{}  (mdist(d;x;a)  +  mdist(d;y;b)))


By

---

Latex:
((Auto  THEN  UseTriangleInequality  [\mkleeneopen{}mdist(d;x;b)\mkleeneclose{}]\mcdot{})
  THEN  (RWO  "mdist-difference"  0  THENA  Auto)
  THEN  (RWO  "mdist-symm"  0  THENA  Auto)
  THEN  (RWO  "mdist-difference"  0  THENA  Auto)
  THEN  nRAdd  \mkleeneopen{}-(mdist(d;b;y))\mkleeneclose{}  0\mcdot{}
  THEN  BLemma  `rleq\_weakening`
  THEN  Auto)

---

Home Index