---

Step * of Lemma real-vec-dist-monotone-in-dim

∀[m:ℕ+]. ∀[p,q:ℝ^m].  (d(p;q) ≤ d(p;q))
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 (GenConcl ⌜p - q = v ∈ ℝ^m⌝⋅ THENA Auto)
   THEN All Thin
   THEN Unfold `dot-product` 0) }

1
1. m : ℕ+
2. v : ℝ^m
⊢ Σ{(v i) * (v i) | 0≤i≤m - 1 - 1} ≤ Σ{(v i) * (v i) | 0≤i≤m - 1}

---

Latex:

---

Latex:
\mforall{}[m:\mBbbN{}\msupplus{}].  \mforall{}[p,q:\mBbbR{}\^{}m].    (d(p;q)  \mleq{}  d(p;q))


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  (GenConcl  \mkleeneopen{}p  -  q  =  v\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Unfold  `dot-product`  0)

---

Home Index