---

Step * of Lemma real-vec-dist-vec-mul

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

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

---

Latex:

---

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


By

---

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

---

Home Index