---

Step * of Lemma real-vec-dist-dilation

∀[n:ℕ]. ∀[x,y:ℝ^n]. ∀[a:ℝ].  (d(a*x;a*y) = (|a| * d(x;y)))
BY
{ (Auto THEN RepUR ``real-vec-dist`` 0) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. a : ℝ
⊢ ||a*x - a*y|| = (|a| * ||x - y||)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].  \mforall{}[a:\mBbbR{}].    (d(a*x;a*y)  =  (|a|  *  d(x;y)))


By

---

Latex:
(Auto  THEN  RepUR  ``real-vec-dist``  0)

---

Home Index