---

Step * of Lemma prod2-metric_wf

∀[X,Y:Type]. ∀[dX:metric(X)]. ∀[dY:metric(Y)].  (prod2-metric(dX;dY) ∈ metric(X × Y))
BY
{ (Intros
   THEN (MemTypeCD THENA Auto)
   THEN All (RepUR ``prod2-metric``)
   THEN Auto
   THEN (DProdsAndUnions THEN All Reduce)
   THEN Auto
   THEN Try ((BLemma `radd_functionality` THEN Auto))
   THEN RWW "mdist-same" 0
   THEN Auto) }

1
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))

---

Latex:

---

Latex:
\mforall{}[X,Y:Type].  \mforall{}[dX:metric(X)].  \mforall{}[dY:metric(Y)].    (prod2-metric(dX;dY)  \mmember{}  metric(X  \mtimes{}  Y))


By

---

Latex:
(Intros
  THEN  (MemTypeCD  THENA  Auto)
  THEN  All  (RepUR  ``prod2-metric``)
  THEN  Auto
  THEN  (DProdsAndUnions  THEN  All  Reduce)
  THEN  Auto
  THEN  Try  ((BLemma  `radd\_functionality`  THEN  Auto))
  THEN  RWW  "mdist-same"  0
  THEN  Auto)

---

Home Index