---

Step * 1 1 of Lemma mdist-max-metric-mul-rleq


1. c : ℝ
2. c' : ℝ
3. n : ℤ
4. 0 < n
5. ∀x:ℝ^n - 1
     (primrec(n - 1;r0;λi,r. rmax(r;|(c * (x i)) - c' * (x i)|)) ≤ (|c - c'| * primrec(n - 1;r0;λi,r. rmax(r;|(x i) - r0\000C|))))
6. x : ℝ^n
7. v : ℝ
8. v1 : ℝ
9. v ≤ (|c - c'| * v1)
10. v ≤ rmax(|c - c'| * v1;|c - c'| * |(x (n - 1)) - r0|)
11. v2 : ℝ
12. (x (n - 1)) = v2 ∈ ℝ
⊢ |(c * v2) - c' * v2| ≤ |(c - c') * (v2 - r0)|
BY
{ (nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(nRNorm  0  THEN  Auto)

---

Home Index