---

Step * of Lemma rleq-real-vec-dist

∀[n:ℕ]. ∀[x,y:ℝ^n]. ∀[i:ℕn].  (|(x i) - y i| ≤ d(x;y))
BY
{ (Auto
   THEN BLemma `square-rleq-implies`
   THEN Auto
   THEN Unfold `real-vec-dist` 0
   THEN (RWO "real-vec-norm-squared" 0 THENA Auto)
   THEN (RWO "rabs-rnexp2" 0 THENA Auto)
   THEN (RWO "rnexp2" 0 THENA Auto)) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. i : ℕn
⊢ (((x i) - y i) * ((x i) - y i)) ≤ x - y⋅x - y

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  BLemma  `square-rleq-implies`
  THEN  Auto
  THEN  Unfold  `real-vec-dist`  0
  THEN  (RWO  "real-vec-norm-squared"  0  THENA  Auto)
  THEN  (RWO  "rabs-rnexp2"  0  THENA  Auto)
  THEN  (RWO  "rnexp2"  0  THENA  Auto))

---

Home Index