---

Step * of Lemma real-vec-dist-from-zero

∀[n:ℕ]. ∀[p:ℝ^n].  (d(p;λi.r0) = ||p||)
BY
{ (Auto THEN RepUR ``real-vec-dist`` 0 THEN BLemma  `real-vec-norm_functionality` THEN Auto) }

1
1. n : ℕ
2. p : ℝ^n
⊢ req-vec(n;p - λi.r0;p)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p:\mBbbR{}\^{}n].    (d(p;\mlambda{}i.r0)  =  ||p||)


By

---

Latex:
(Auto  THEN  RepUR  ``real-vec-dist``  0  THEN  BLemma    `real-vec-norm\_functionality`  THEN  Auto)

---

Home Index