---

Step * 2 of Lemma mdist_functionality


1. X : Type
2. d : metric(X)
3. x : X
4. y : X
5. x' : X
6. y' : X
7. mdist(d;y;y') = r0
8. mdist(d;x;x') = r0
⊢ mdist(d;x';y') ≤ mdist(d;x;y)
BY
{ UseMetricTriangleInequality [⌜x⌝;⌜y⌝]⋅ }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  x  :  X
4.  y  :  X
5.  x'  :  X
6.  y'  :  X
7.  mdist(d;y;y')  =  r0
8.  mdist(d;x;x')  =  r0
\mvdash{}  mdist(d;x';y')  \mleq{}  mdist(d;x;y)


By

---

Latex:
UseMetricTriangleInequality  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}

---

Home Index