---

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

∀[n:ℕ]. ∀[x:ℝ^n]. ∀[c,c':ℝ].  (mdist(max-metric(n);c*x;c'*x) ≤ (|c - c'| * mdist(max-metric(n);x;λi.r0)))
BY
{ (Intros
   THEN RepUR ``mdist max-metric real-vec-mul`` 0
   THEN (Unhide THENA Auto)
   THEN NatInd 1
   THEN Reduce 0
   THEN Auto
   THEN (RWO  "primrec-unroll" 0 THENA Auto)
   THEN (OReduce 0 THENA Auto)
   THEN (InstHyp [⌜x⌝] (-2)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN ((GenConclAtAddrType ⌜ℝ⌝ [1;1]⋅ THENA Auto) THEN Thin (-1))
   THEN (GenConclAtAddrType ⌜ℝ⌝ [1;2;2]⋅ THENA Auto)
   THEN Thin (-1)
   THEN (D 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)
⊢ rmax(v;|(c * (x (n - 1))) - c' * (x (n - 1))|) ≤ (|c - c'| * rmax(v1;|(x (n - 1)) - r0|))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbR{}\^{}n].  \mforall{}[c,c':\mBbbR{}].
    (mdist(max-metric(n);c*x;c'*x)  \mleq{}  (|c  -  c'|  *  mdist(max-metric(n);x;\mlambda{}i.r0)))


By

---

Latex:
(Intros
  THEN  RepUR  ``mdist  max-metric  real-vec-mul``  0
  THEN  (Unhide  THENA  Auto)
  THEN  NatInd  1
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO    "primrec-unroll"  0  THENA  Auto)
  THEN  (OReduce  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  ((GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;1]\mcdot{}  THENA  Auto)  THEN  Thin  (-1))
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;2;2]\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (D  0  THENA  Auto))

---

Home Index