---

Step * of Lemma real-vec-norm-positive-iff2

∀n:ℕ. ∀x:ℝ^n.  (∃i:ℕn. x i ≠ r0 ⇐⇒ r0 < ||x||)
BY
{ (RWO "real-vec-norm-positive-iff" 0 THEN Auto THEN ParallelLast THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x:\mBbbR{}\^{}n.    (\mexists{}i:\mBbbN{}n.  x  i  \mneq{}  r0  \mLeftarrow{}{}\mRightarrow{}  r0  <  ||x||)


By

---

Latex:
(RWO  "real-vec-norm-positive-iff"  0  THEN  Auto  THEN  ParallelLast  THEN  EAuto  1)

---

Home Index