---

Step * of Lemma real-vec-dist-sub-zero

∀[n:ℕ]. ∀[p,q:ℝ^n].  (d(p - q;λi.r0) = d(p;q))
BY
{ (Auto THEN InstLemma `real-vec-dist-translation` [⌜n⌝;⌜p⌝;⌜q⌝;⌜q⌝]⋅ THEN Auto) }

1
1. n : ℕ
2. p : ℝ^n
3. q : ℝ^n
4. d(p - q;q - q) = d(p;q)
⊢ d(p - q;λi.r0) = d(p;q)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p,q:\mBbbR{}\^{}n].    (d(p  -  q;\mlambda{}i.r0)  =  d(p;q))


By

---

Latex:
(Auto  THEN  InstLemma  `real-vec-dist-translation`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index