---

Step * 1 of Lemma prod2-metric_wf


1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. ∀x,y:X × Y.  (r0 ≤ let x1,y1 = x in let x2,y2 = y in mdist(dX;x1;x2) + mdist(dY;y1;y2))
6. x1 : X
7. x2 : Y
8. y1 : X
9. y2 : Y
10. z1 : X
11. z2 : Y
⊢ (mdist(dX;x1;z1) + mdist(dY;x2;z2)) ≤ ((mdist(dX;x1;y1) + mdist(dY;x2;y2)) + mdist(dX;z1;y1) + mdist(dY;z2;y2))
BY
{ ((Assert ((mdist(dX;x1;y1) + mdist(dY;x2;y2)) + mdist(dX;z1;y1) + mdist(dY;z2;y2))
          = ((mdist(dX;x1;y1) + mdist(dX;z1;y1)) + mdist(dY;x2;y2) + mdist(dY;z2;y2)) BY
          Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN BLemma `radd_functionality_wrt_rleq`
   THEN Auto
   THEN RW (AddrC [2;2] (LemmaC `mdist-symm`)) 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  Y  :  Type
3.  dX  :  metric(X)
4.  dY  :  metric(Y)
5.  \mforall{}x,y:X  \mtimes{}  Y.    (r0  \mleq{}  let  x1,y1  =  x  in  let  x2,y2  =  y  in  mdist(dX;x1;x2)  +  mdist(dY;y1;y2))
6.  x1  :  X
7.  x2  :  Y
8.  y1  :  X
9.  y2  :  Y
10.  z1  :  X
11.  z2  :  Y
\mvdash{}  (mdist(dX;x1;z1)  +  mdist(dY;x2;z2))  \mleq{}  ((mdist(dX;x1;y1)  +  mdist(dY;x2;y2))
+  mdist(dX;z1;y1)
+  mdist(dY;z2;y2))


By

---

Latex:
((Assert  ((mdist(dX;x1;y1)  +  mdist(dY;x2;y2))  +  mdist(dX;z1;y1)  +  mdist(dY;z2;y2))
                =  ((mdist(dX;x1;y1)  +  mdist(dX;z1;y1))  +  mdist(dY;x2;y2)  +  mdist(dY;z2;y2))  BY
                Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  BLemma  `radd\_functionality\_wrt\_rleq`
  THEN  Auto
  THEN  RW  (AddrC  [2;2]  (LemmaC  `mdist-symm`))  0
  THEN  Auto)

---

Home Index