---

Step * 1 of Lemma mdist-max-metric-mul2


1. c : ℝ
2. n : ℤ
3. 0 < n
4. ∀p,q:ℝ^n - 1.
     (primrec(n - 1;r0;λi,r. rmax(r;|(c * (p i)) - c * (q i)|)) = (|c| * primrec(n - 1;r0;λi,r. rmax(r;|(p i) - q i|))))
5. p : ℝ^n
6. q : ℝ^n
7. v : ℝ
8. v1 : ℝ
9. v = (|c| * v1)
⊢ rmax(v;|(c * (p (n - 1))) - c * (q (n - 1))|) = (|c| * rmax(v1;|(p (n - 1)) - q (n - 1)|))
BY
{ (RWO  "rmul-rmax" 0
   THEN Auto
   THEN BLemma `rmax_functionality`
   THEN Auto
   THEN (RWO "rabs-rmul<" 0 THENM nRNorm 0)
   THEN Auto) }

---

Latex:

---

Latex:

1.  c  :  \mBbbR{}
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}p,q:\mBbbR{}\^{}n  -  1.
          (primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(c  *  (p  i))  -  c  *  (q  i)|))
          =  (|c|  *  primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(p  i)  -  q  i|))))
5.  p  :  \mBbbR{}\^{}n
6.  q  :  \mBbbR{}\^{}n
7.  v  :  \mBbbR{}
8.  v1  :  \mBbbR{}
9.  v  =  (|c|  *  v1)
\mvdash{}  rmax(v;|(c  *  (p  (n  -  1)))  -  c  *  (q  (n  -  1))|)  =  (|c|  *  rmax(v1;|(p  (n  -  1))  -  q  (n  -  1)|))


By

---

Latex:
(RWO    "rmul-rmax"  0
  THEN  Auto
  THEN  BLemma  `rmax\_functionality`
  THEN  Auto
  THEN  (RWO  "rabs-rmul<"  0  THENM  nRNorm  0)
  THEN  Auto)

---

Home Index