---

Step * of Lemma mdist-rn-metric-mul

∀[n:ℕ]. ∀[p:ℝ^n]. ∀[c:ℝ].  (mdist(rn-metric(n);c*p;λi.r0) = (|c| * mdist(rn-metric(n);p;λi.r0)))
BY
{ (Intros THEN RepUR ``mdist rn-metric`` 0 THEN RWO "real-vec-dist-from-zero" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  RepUR  ``mdist  rn-metric``  0  THEN  RWO  "real-vec-dist-from-zero"  0  THEN  Auto)

---

Home Index