---

Step * 1 1 of Lemma proj-norm-positive


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

---

Latex:

---

Latex:

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


By

---

Latex:
EAuto  1

---

Home Index