---

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

No Annotations
∀[n:ℕ]. ∀[x:ℝ^n]. ∀[c:ℝ].  ((∀i:ℕn. (|x i| ≤ c)) ⇒ (||x|| ≤ (rsqrt(r(n)) * c)))
BY
{ (Auto THEN CaseNat 0 `n') }

1
1. n : ℕ
2. x : ℝ^n
3. c : ℝ
4. ∀i:ℕn. (|x i| ≤ c)
5. n = 0 ∈ ℤ
⊢ ||x|| ≤ (rsqrt(r0) * c)

2
1. n : ℕ
2. x : ℝ^n
3. c : ℝ
4. ∀i:ℕn. (|x i| ≤ c)
5. ¬(n = 0 ∈ ℤ)
⊢ ||x|| ≤ (rsqrt(r(n)) * c)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbR{}\^{}n].  \mforall{}[c:\mBbbR{}].    ((\mforall{}i:\mBbbN{}n.  (|x  i|  \mleq{}  c))  {}\mRightarrow{}  (||x||  \mleq{}  (rsqrt(r(n))  *  c)))


By

---

Latex:
(Auto  THEN  CaseNat  0  `n')

---

Home Index