---

Step * 2 1 of Lemma real-vec-dist-identity


1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. req-vec(n;x;y)
5. ||x - y|| = ||r0*x||
⊢ ||x - y|| = r0
BY
{ (RWW "-1 real-vec-norm-mul rabs-of-nonneg" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbR{}\^{}n
3.  y  :  \mBbbR{}\^{}n
4.  req-vec(n;x;y)
5.  ||x  -  y||  =  ||r0*x||
\mvdash{}  ||x  -  y||  =  r0


By

---

Latex:
(RWW  "-1  real-vec-norm-mul  rabs-of-nonneg"  0  THEN  Auto)

---

Home Index