---

Step * of Lemma rn-metric-leq-rn-prod-metric

∀[n:ℕ]. rn-metric(n) ≤ rn-prod-metric(n)
BY
{ (RepUR ``metric-leq mdist max-metric rn-metric`` 0
   THEN Fold `mdist` 0
   THEN Auto
   THEN BLemma `square-rleq-implies`
   THEN Auto
   THEN Unfold `real-vec-dist` 0
   THEN (RWO "real-vec-norm-squared" 0 THENA Auto)
   THEN RepUR ``mdist rn-prod-metric prod-metric rmetric`` 0
   THEN (Subst' Σ{|(x i) - y i| | 0≤i≤n - 1} ~ Σ{|x - y i| | 0≤i≤n - 1} 0 THENA (RepUR ``real-vec-sub`` 0 THEN Auto))
   THEN (GenConclTerm ⌜x - y⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. n : ℕ
2. v : ℝ^n
⊢ v⋅v ≤ Σ{|v i| | 0≤i≤n - 1}^2

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  rn-metric(n)  \mleq{}  rn-prod-metric(n)


By

---

Latex:
(RepUR  ``metric-leq  mdist  max-metric  rn-metric``  0
  THEN  Fold  `mdist`  0
  THEN  Auto
  THEN  BLemma  `square-rleq-implies`
  THEN  Auto
  THEN  Unfold  `real-vec-dist`  0
  THEN  (RWO  "real-vec-norm-squared"  0  THENA  Auto)
  THEN  RepUR  ``mdist  rn-prod-metric  prod-metric  rmetric``  0
  THEN  (Subst'  \mSigma{}\{|(x  i)  -  y  i|  |  0\mleq{}i\mleq{}n  -  1\}  \msim{}  \mSigma{}\{|x  -  y  i|  |  0\mleq{}i\mleq{}n  -  1\}  0
              THENA  (RepUR  ``real-vec-sub``  0  THEN  Auto)
              )
  THEN  (GenConclTerm  \mkleeneopen{}x  -  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index