---

Step * of Lemma mdist-max-metric-mul

∀[n:ℕ]. ∀[p:ℝ^n]. ∀[c:ℝ].  (mdist(max-metric(n);c*p;λi.r0) = (|c| * mdist(max-metric(n);p;λi.r0)))
BY
{ (Intros
   THEN (Assert λi.r0 ∈ ℝ^n BY
               Auto)
   THEN (RWO  "mdist-max-metric-mul2<" 0 THENA Auto)
   THEN BLemma `mdist_functionality`
   THEN Auto
   THEN BLemma `meq-max-metric`
   THEN Auto) }

1
1. n : ℕ
2. p : ℝ^n
3. c : ℝ
4. λi.r0 ∈ ℝ^n
⊢ req-vec(n;λi.r0;c*λi.r0)

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (Assert  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}n  BY
                          Auto)
  THEN  (RWO    "mdist-max-metric-mul2<"  0  THENA  Auto)
  THEN  BLemma  `mdist\_functionality`
  THEN  Auto
  THEN  BLemma  `meq-max-metric`
  THEN  Auto)

---

Home Index