---

Step * 1 1 of Lemma meq-max-metric-iff-meq-rn-metric


1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. max-metric(n) ≤ rn-metric(n)
5. mdist(max-metric(n);x;y) = r0
6. mdist(rn-metric(n);x;y) ≤ mdist(r(n)*max-metric(n);x;y)
⊢ mdist(r(n)*max-metric(n);x;y) ≤ r0
BY
{ (RepUR ``mdist scale-metric`` 0 THEN Fold `mdist` 0 THEN RWO "5" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbR{}\^{}n
3.  y  :  \mBbbR{}\^{}n
4.  max-metric(n)  \mleq{}  rn-metric(n)
5.  mdist(max-metric(n);x;y)  =  r0
6.  mdist(rn-metric(n);x;y)  \mleq{}  mdist(r(n)*max-metric(n);x;y)
\mvdash{}  mdist(r(n)*max-metric(n);x;y)  \mleq{}  r0


By

---

Latex:
(RepUR  ``mdist  scale-metric``  0  THEN  Fold  `mdist`  0  THEN  RWO  "5"  0  THEN  Auto)

---

Home Index