---

Step * of Lemma mdist-max-metric-mul2

∀[n:ℕ]. ∀[p,q:ℝ^n]. ∀[c:ℝ].  (mdist(max-metric(n);c*p;c*q) = (|c| * mdist(max-metric(n);p;q)))
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 [⌜p⌝;⌜q⌝] (-3)⋅ 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. 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)|))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p,q:\mBbbR{}\^{}n].  \mforall{}[c:\mBbbR{}].    (mdist(max-metric(n);c*p;c*q)  =  (|c|  *  mdist(max-metric(n);p;q)))


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{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]  (-3)\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