---

Step * 1 of Lemma proj-norm-positive


1. n : ℕ
2. a : ℝ^n + 1
3. ∃k:ℕn + 1. a k ≠ r0
⊢ r0 < ||a||
BY
{ ((BLemma `real-vec-norm-positive-iff` THEN Auto) THEN ParallelLast) }

1
1. n : ℕ
2. a : ℝ^n + 1
3. k : ℕn + 1
4. a k ≠ r0
⊢ r0 ≠ a k

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n  +  1
3.  \mexists{}k:\mBbbN{}n  +  1.  a  k  \mneq{}  r0
\mvdash{}  r0  <  ||a||


By

---

Latex:
((BLemma  `real-vec-norm-positive-iff`  THEN  Auto)  THEN  ParallelLast)

---

Home Index