---

Step * of Lemma component-rleq-real-vec-norm

∀n:ℕ. ∀i:ℕn. ∀x:ℝ^n.  (|x i| ≤ ||x||)
BY
{ (Auto
   THEN (BLemma `square-rleq-implies` THEN Auto)
   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. i : ℕn
3. x : ℝ^n
⊢ ((x i) * (x i)) ≤ x⋅x

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.  \mforall{}x:\mBbbR{}\^{}n.    (|x  i|  \mleq{}  ||x||)


By

---

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

---

Home Index