---

Step * 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)
⊢ rmax(v;|(c * (x (n - 1))) - c' * (x (n - 1))|) ≤ (|c - c'| * rmax(v1;|(x (n - 1)) - r0|))
BY
{ ((RWO "rmul-rmax" 0 THENA Auto)
   THEN (BLemma `rmax_lb` THEN Auto)
   THEN BLemma `rmax_ub`
   THEN Auto
   THEN OrRight
   THEN Auto
   THEN (GenConclTerm ⌜x (n - 1)⌝⋅ THENA Auto)
   THEN (RWO "rabs-rmul<" 0 THENA Auto)) }

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

---

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)
\mvdash{}  rmax(v;|(c  *  (x  (n  -  1)))  -  c'  *  (x  (n  -  1))|)  \mleq{}  (|c  -  c'|  *  rmax(v1;|(x  (n  -  1))  -  r0|))


By

---

Latex:
((RWO  "rmul-rmax"  0  THENA  Auto)
  THEN  (BLemma  `rmax\_lb`  THEN  Auto)
  THEN  BLemma  `rmax\_ub`
  THEN  Auto
  THEN  OrRight
  THEN  Auto
  THEN  (GenConclTerm  \mkleeneopen{}x  (n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "rabs-rmul<"  0  THENA  Auto))

---

Home Index