---

Step * of Lemma implies-real-vec-dist-rleq

∀[n:ℕ]. ∀[x,y:ℝ^n]. ∀[c:ℝ].  ((∀i:ℕn. (|(x i) - y i| ≤ c)) ⇒ (d(x;y) ≤ (rsqrt(r(n)) * c)))
BY
{ (Auto
   THEN Unfold `real-vec-dist` 0
   THEN BLemma `implies-real-vec-norm-rleq`
   THEN Auto
   THEN RepUR ``real-vec-sub`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].  \mforall{}[c:\mBbbR{}].    ((\mforall{}i:\mBbbN{}n.  (|(x  i)  -  y  i|  \mleq{}  c))  {}\mRightarrow{}  (d(x;y)  \mleq{}  (rsqrt(r(n))  *  c)))


By

---

Latex:
(Auto
  THEN  Unfold  `real-vec-dist`  0
  THEN  BLemma  `implies-real-vec-norm-rleq`
  THEN  Auto
  THEN  RepUR  ``real-vec-sub``  0
  THEN  Auto)

---

Home Index