---

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


1. n : ℕ
2. v : ℝ^n
⊢ v⋅v ≤ Σ{|v i| | 0≤i≤n - 1}^2
BY
{ (NatInd 1 THENL [(Unfold `dot-product` 0 THEN RWO "rsum-empty" 0 THEN Auto); Auto]) }

1
1. n : ℤ
2. 0 < n
3. ∀v:ℝ^n - 1. (v⋅v ≤ Σ{|v i| | 0≤i≤n - 1 - 1}^2)
4. v : ℝ^n
⊢ v⋅v ≤ Σ{|v i| | 0≤i≤n - 1}^2

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  v  :  \mBbbR{}\^{}n
\mvdash{}  v\mcdot{}v  \mleq{}  \mSigma{}\{|v  i|  |  0\mleq{}i\mleq{}n  -  1\}\^{}2


By

---

Latex:
(NatInd  1  THENL  [(Unfold  `dot-product`  0  THEN  RWO  "rsum-empty"  0  THEN  Auto);  Auto])

---

Home Index