---

Step * of Lemma real-vec-dist_functionality

∀[n:ℕ]. ∀[x1,x2,y1,y2:ℝ^n].  (d(x1;y1) = d(x2;y2)) supposing (req-vec(n;x1;x2) and req-vec(n;y1;y2))
BY
{ (Auto THEN Unfold `real-vec-dist` 0) }

1
1. n : ℕ
2. x1 : ℝ^n
3. x2 : ℝ^n
4. y1 : ℝ^n
5. y2 : ℝ^n
6. req-vec(n;y1;y2)
7. req-vec(n;x1;x2)
⊢ ||x1 - y1|| = ||x2 - y2||

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x1,x2,y1,y2:\mBbbR{}\^{}n].    (d(x1;y1)  =  d(x2;y2))  supposing  (req-vec(n;x1;x2)  and  req-vec(n;y1;y2))


By

---

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

---

Home Index