---

Step * 1 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