---

Step * of Lemma real-vec-dist-identity

∀[n:ℕ]. ∀[x,y:ℝ^n].  uiff(d(x;y) = r0;req-vec(n;x;y))
BY
{ Auto }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. d(x;y) = r0
⊢ req-vec(n;x;y)

2
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. req-vec(n;x;y)
⊢ d(x;y) = r0

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    uiff(d(x;y)  =  r0;req-vec(n;x;y))


By

---

Latex:
Auto

---

Home Index