---

Step * 1 of Lemma metric-leq-meq


1. X : Type
2. d1 : metric(X)
3. d2 : metric(X)
4. d1 ≤ d2
5. x : X
6. y : X
7. mdist(d2;x;y) = r0
8. mdist(d1;x;y) ≤ mdist(d2;x;y)
⊢ mdist(d1;x;y) = r0
BY
{ ((Assert r0 ≤ mdist(d1;x;y) BY Auto) THEN EAuto 1) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  r0  \mleq{}  mdist(d1;x;y)  BY  Auto)  THEN  EAuto  1)

---

Home Index